
Eq = λA::*.λB::*.∀P::* ⇒ *.P A → P B;

refl : ∀A.Eq A A = ΛA::*.ΛP::*⇒*.λx:P A.x;

symm = ΛA::*.ΛB::*.λe:Eq A B.e [λX::*.Eq X A] (refl [A]);

trans = ΛA::*.ΛB::*.ΛC::*.λab:Eq A B.λbc:Eq B C. bc [Eq A] ab;

lift = ΛA::*.ΛB::*.ΛP::* ⇒ *.λe:Eq A B.e [λX::*.Eq (P A) (P X)] (refl [P A]);
