:let id    = \(A : Set) (x : A) -> x
:let const = \(A B : Set) (x : A) (y : B) -> x
:let flip  = \(A B C : Set) (f : A -> B -> C) (y : B) (x : A) -> f x y
:let Tup = \(A B : Set) -> (R : Set) -> (A -> B -> R) -> R
:let tup = \(A B : Set) (x : A) (y : B) (R : Set) (f : A -> B -> R) -> f x y
:let fst = \(A B : Set) (p : Tup A B) -> p A (const A B)
:let snd = \(A B : Set) (p : Tup A B) -> p B (flip B A B (const B A))

:let Nat = (R : Set) -> (R -> R) -> R -> R
:let zero = \(R : Set) (s : R -> R) (z : R) -> z
:let suc  = \(n : Nat) (R : Set) (s : R -> R) (z : R) -> s (n R s z)
:let plus = \(m n : Nat) (R : Set) (s : R -> R) (z : R) -> m R s (n R s z)
:let times = \(m n : Nat) (R : Set) (s : R -> R) (z : R) -> m R (n R s) z

:let List = \(A : Set) -> (R : Set) -> (A -> R -> R) -> R -> R
:let nil = \(A R : Set) (f : A -> R -> R) (z : R) -> z
:let cons = \(A : Set) (x : A) (xs : List A) (R : Set) (f : A -> R -> R) (z : R) -> f x (xs R f z)