Leibniz.java

public interface Leibniz<A, B> extends  __2<Leibniz.µ, A, B> {
  enum µ {}

  <f> __<f, B> subst(__<f, A> p);

  static <T> Leibniz<T, T> refl() { return HktId::id; }

  default B coerce(A a) {
    return _Leibniz.asId(subst((Id<A>) () -> a)).__();
  }

  default <f> Leibniz<__<f, A>, __<f, B>> lift() {
    final Lift<f, A, A> _refl = Leibniz::refl;

    return _Leibniz.asLift(subst(_refl)).__();
  }

  default <f, C> Leibniz<__<__<f, A>, C>, __<__<f, B>, C>> lift2() {
    return lift2(refl());
  }

  default <f, C, D> Leibniz<__<__<f, A>, C>, __<__<f, B>, D>> lift2(Leibniz<C, D> cd) {
    final Lift2_1<f, A, C, A> _refl = Leibniz::refl;

    final Lift2_1<f, A, C, B> lift2_1 = _Leibniz.asLift2_1(subst(_refl));

    final Lift2<f, A, C, B, C> lift2 = () -> lift2_1.__();

    return _Leibniz.asLift2(cd.subst(lift2)).__();
  }

  default <f, C, D> Leibniz<__<__<__<f, A>, C>, D>, __<__<__<f, B>, C>, D>> lift3() {
    return lift3(refl(), refl());
  }

  default <f, C, D, E, F> Leibniz<__<__<__<f, A>, C>, E>, __<__<__<f, B>, D>, F>> lift3(Leibniz<C, D> cd
    , Leibniz<E, F> ef) {
    final Lift3_1<f, A, C, E, A> _refl = Leibniz::refl;

    final Lift3_1<f, A, C, E, B> lift3_1 = _Leibniz.asLift3_1(subst(_refl));

    final Lift3_2<f, A, C, E, B, C> lift3_2 = () -> lift3_1.__();

    final Lift3_2<f, A, C, E, B, D> lift3_2_1 = _Leibniz.asLift3_2(cd.subst(lift3_2));

    final Lift3<f, A, C, E, B, D, E> lift3 = () -> lift3_2_1.__();

    return _Leibniz.asLift3(ef.subst(lift3)).__();
  }
}

interface HktId {
  static <f, T> __<f, T> id(__<f, T> ft) { return ft; }
}

interface $<A> { A __(); }

@HktConfig(generateIn = "_Leibniz", withVisibility = Package)
interface Id<A> extends $<A>, __<Id.µ, A> { enum µ {} }

@HktConfig(generateIn = "_Leibniz", withVisibility = Package)
interface Lift<f, A, B> extends $<Leibniz<__<f, A>, __<f, B>>>
  , __3<Lift.µ, f, A, B> { enum µ {} }

@HktConfig(generateIn = "_Leibniz", withVisibility = Package)
interface Lift2_1<f, A, B, X> extends $<Leibniz<__<__<f, A>, B>, __<__<f, X>, B>>>
  , __4<Lift2_1.µ, f, A, B, X> { enum µ {} }

@HktConfig(generateIn = "_Leibniz", withVisibility = Package)
interface Lift2<f, A, B, C, X> extends $<Leibniz<__<__<f, A>, B>, __<__<f, C>, X>>>
  , __5<Lift2.µ, f, A, B, C, X>  { enum µ {} }

@HktConfig(generateIn = "_Leibniz", withVisibility = Package)
interface Lift3_1<f, A, B, C, X> extends $<Leibniz<__<__<__<f, A>, B>, C>, __<__<__<f, X>, B>, C>>>
  , __5<Lift3_1.µ, f, A, B, C, X> { enum µ {} }

@HktConfig(generateIn = "_Leibniz", withVisibility = Package)
interface Lift3_2<f, A, B, C, D, X> extends $<Leibniz<__<__<__<f, A>, B>, C>, __<__<__<f, D>, X>, C>>>
  , __6<Lift3_2.µ, f, A, B, C, D, X> { enum µ {} }

@HktConfig(generateIn = "_Leibniz", withVisibility = Package)
interface Lift3<f, A, B, C, D, E, X> extends $<Leibniz<__<__<__<f, A>, B>, C>, __<__<__<f, D>, E>, X>>>
  , __7<Lift3.µ, f, A, B, C, D, E, X> { enum µ {} }