Nat :: *
    = ∀α::*.α → (α → α) → α;

zero : Nat
     = Λα::*.λz:α.λs:α → α.z;

succ : Nat → Nat
     = λn:Nat.Λα::*.λz:α.λs:α → α.s (n [α] z s);

add : Nat → Nat → Nat
    = λm:Nat.λn:Nat.m [Nat] n succ;

Eq :: * ⇒ * ⇒ *
    = λα::*.λβ::*.∀φ::*⇒*.φ α → φ β;

refl : ∀α.Eq α α
     = Λα::*.Λφ::*⇒*.λx:φ α.x;

symm : ∀α.∀β.Eq α β → Eq β α
     = Λα.Λβ.λab:Eq α β.Λφ::*⇒*.λx:φ β.ab [λZ.φ Z → φ α] (λy:φ α.y) x;

trans : ∀α.∀β.∀γ.Eq α β → Eq β γ → Eq α γ
      = Λα.Λβ.Λγ.λab:Eq α β.λbc:Eq β γ.Λφ::*⇒*.λx:φ α.bc [φ] (ab [φ] x);

### Question 2 ###

# Tree :: ...
#      = ...

# leaf : ...
#      = ...

# branch : ...
#        = ...

# totalNatTree : ...
#              = ...

### Question 3 ###

# Equal :: ...
#       = ...

# reflEqual : ...
#           = ...

# symmEqual : ...
#           = ...

# transEqual : ...
#            = ...

# toLeibniz : ...
#           = ...

# fromLeibniz : ...
#             = ...
