-- This does not type check because it lacks a whnf

inconsistent
: {P : Type} P
= inconsistent

-- Identity

the
: {A : Type} {u : A} A
= [A] [u] u

-- A self-referential type

Self
: {T : (Self T)} Type
= [T] {self : (T self)} Type

-- The empty, uninhabited type

Empty
: (Self Empty)
= [self]
  {Prop : (Self Empty)}
  (Prop self)

-- The unit type

Unit
: (Self Unit)
= [self]
  {Prop : (Self Unit)}
  {new  : (Prop Unit.new)}
  (Prop self)

Unit.new
: (Unit Unit.new)
= [Prop] [new] new

-- The booleans true and false

Bool
: (Self Bool)
= [self]
  {Prop  : (Self Bool)}
  {true  : (Prop Bool.true)}
  {false : (Prop Bool.false)}
  (Prop self)

Bool.true
: (Bool Bool.true)
= [Prop] [true] [false] true

Bool.false
: (Bool Bool.false)
= [Prop] [true] [false] false

Bool.induct
: {self  : (Bool self)}
  {Prop  : (Self Bool)}
  {true  : (Prop Bool.true)}
  {false : (Prop Bool.false)}
  (Prop self)
= [self] [Prop] [true] [false]
  (self Prop true false)

Bool.not
: {self : (Bool self)} (Bool (Bool.not self))
= [self]
  (self
    [self] (Bool (Bool.not self))
    Bool.false
    Bool.true)

-- Natural numbers (Scott)

Nat
: (Self Nat)
= [self]
  {Prop : (Self Nat)}
  {succ : {pred : (Nat pred)} (Prop (Nat.succ pred))}
  {zero : (Prop Nat.zero)}
  (Prop self)

Nat.succ
: {pred : (Nat pred)} (Nat (Nat.succ pred))
= [pred] [Nat.] [succ.] [zero.]
  (succ. pred)

Nat.zero
: (Nat Nat.zero)
= [Nat.] [succ.] [zero.] zero.

Nat.0 : (Nat Nat.0) = Nat.zero
Nat.1 : (Nat Nat.1) = (Nat.succ Nat.0)
Nat.2 : (Nat Nat.2) = (Nat.succ Nat.1)
Nat.3 : (Nat Nat.3) = (Nat.succ Nat.2)
Nat.4 : (Nat Nat.4) = (Nat.succ Nat.3)
Nat.5 : (Nat Nat.5) = (Nat.succ Nat.4)
Nat.6 : (Nat Nat.6) = (Nat.succ Nat.5)
Nat.7 : (Nat Nat.7) = (Nat.succ Nat.6)
Nat.8 : (Nat Nat.8) = (Nat.succ Nat.7)
Nat.9 : (Nat Nat.9) = (Nat.succ Nat.8)

Nat.id
: {a : (Nat a)} (Nat (Nat.id a))
= [a]
  (a
    [a] (Nat (Nat.id a))
    [pred] (Nat.succ (Nat.id pred))
    Nat.zero)

Nat.same
: {a : (Nat a)} (Nat (Nat.same a))
= [a] [Prop] [succ] [zero]
  (a [a] (Prop (Nat.same a))
    [pred] (succ (Nat.same pred))
    zero)

Nat.double
: {n : (Nat n)} (Nat (Nat.double n))
= [n]
  (n [n] (Nat (Nat.double n))
    [pred] (Nat.succ (Nat.succ (Nat.double pred)))
    Nat.zero)

Nat.add
: {a : (Nat a)} {b : (Nat b)} (Nat (Nat.add a b))
= [a] [b] (a
  [a] (Nat (Nat.add a b))
  [a] (Nat.succ (Nat.add a b))
  b)

Nat.add_zero_r
: {a : (Nat a)} (Eq Nat (Nat.add a Nat.zero) a (Nat.add_zero_r a))
= [a]
  (a
    [self] (Eq Nat (Nat.add self Nat.zero) self (Nat.add_zero_r self))
    [pred] (Eq.cong Nat Nat (Nat.add pred Nat.zero) pred (Nat.add_zero_r pred) Nat.succ)
    (Eq.refl Nat Nat.zero))

Nat.add_succ_r
: {a : (Nat a)} {b : (Nat b)} (Eq Nat (Nat.add a (Nat.succ b)) (Nat.succ (Nat.add a b)) (Nat.add_succ_r a b))
= [a] [b]
  (a
    [self] (Eq Nat (Nat.add self (Nat.succ b)) (Nat.succ (Nat.add self b)) (Nat.add_succ_r self b))
    [pred] (Eq.cong Nat Nat (Nat.add pred (Nat.succ b)) (Nat.succ (Nat.add pred b)) (Nat.add_succ_r pred b) Nat.succ)
    (Eq.refl Nat (Nat.succ b)))

Nat.add_comm
: {a : (Nat a)} {b : (Nat b)} (Eq Nat (Nat.add a b) (Nat.add b a) (Nat.add_comm a b))
= [a : (Nat a)]
  (a
    [self] {b : (Nat b)} (Eq Nat (Nat.add self b) (Nat.add b self) (Nat.add_comm self b))
    [pred] [b]
      (Eq.subst Nat
	(Nat.add b pred) (Nat.add pred b) (Eq.sym Nat (Nat.add pred b) (Nat.add b pred) (Nat.add_comm pred b))
	[x : (Nat x)] (Eq Nat (Nat.succ x) (Nat.add b (Nat.succ pred)))
	(Eq.sym Nat (Nat.add b (Nat.succ pred)) (Nat.succ (Nat.add b pred)) (Nat.add_succ_r b pred)))
    [b] (Eq.sym Nat (Nat.add b Nat.zero) b (Nat.add_zero_r b)))


Nat.add_assoc
: {a : (Nat a)} {b : (Nat b)} {c : (Nat c)} (Eq Nat (Nat.add (Nat.add a b) c) (Nat.add a (Nat.add b c)) (Nat.add_assoc a b c))
= [a] [b] [c]
  let motive [self]
    (Eq Nat (Nat.add (Nat.add self b) c) (Nat.add self (Nat.add b c)) (Nat.add_assoc self b c))
  let case_succ [a]
    let ab_c (Nat.add (Nat.add a b) c)
    let a_bc (Nat.add a (Nat.add b c))
    (Eq.cong Nat Nat ab_c a_bc (Nat.add_assoc a b c) Nat.succ)
  let case_zero
    (Eq.refl Nat (Nat.add b c))
(a motive case_succ case_zero)

Nat.add_assoc_r
: {a : (Nat a)} {b : (Nat b)} {c : (Nat c)} (Eq Nat (Nat.add a (Nat.add b c)) (Nat.add (Nat.add a b) c) (Nat.add_assoc_r a b c))
= [a] [b] [c]
  (Eq.sym Nat (Nat.add (Nat.add a b) c) (Nat.add a (Nat.add b c)) (Nat.add_assoc a b c))

-- Proof that `a + (b + c) = b + (a + c)`
Nat.add_swap
: {a : (Nat a)} {b : (Nat b)} {c : (Nat c)} (Eq Nat (Nat.add a (Nat.add b c)) (Nat.add b (Nat.add a c)) (Nat.add_swap a b c))
= [a] [b] [c]
  (Eq.r_trans Nat
    (Nat.add a (Nat.add b c)) (Nat.add (Nat.add a b) c) (Nat.add b (Nat.add a c)) (Nat.add_assoc a b c)
    (Eq.trans Nat (Nat.add (Nat.add a b) c) (Nat.add (Nat.add b a) c) (Nat.add b (Nat.add a c))
      (Eq.cong Nat Nat (Nat.add a b) (Nat.add b a) (Nat.add_comm a b) [x : (Nat x)] (Nat.add x c))
      (Nat.add_assoc b a c)))

Nat.mul
: {a : (Nat a)} {b : (Nat b)} (Nat (Nat.mul a b))
= [a] [b]
  (a [a] (Nat (Nat.mul a b))
    [pred] (Nat.add b (Nat.mul pred b))
    Nat.zero)

Nat.mul_zero_r
: {a : (Nat a)} (Eq Nat (Nat.mul a Nat.zero) Nat.zero (Nat.mul_zero_r a))
= [a]
  let motive [self]
    (Eq Nat (Nat.mul self Nat.zero) Nat.zero (Nat.mul_zero_r self))
  let case_succ [a]
    (Eq.cong Nat Nat (Nat.mul a Nat.zero) Nat.zero (Nat.mul_zero_r a) (Nat.add Nat.zero))
  let case_zero
    (Eq.refl Nat Nat.zero)
  (a motive case_succ case_zero)

Nat.mul_one_r
: {a : (Nat a)} (Eq Nat (Nat.mul a (Nat.succ Nat.zero)) a (Nat.mul_one_r a))
= [a]
  let motive [self]
    (Eq Nat (Nat.mul self (Nat.succ Nat.zero)) self (Nat.mul_a_one self))
  let case_succ [a]
    (Eq.cong Nat Nat (Nat.mul a (Nat.succ Nat.zero)) a (Nat.mul_one_r a) Nat.succ)
  let case_zero
    (Eq.refl Nat Nat.zero)
  (a motive case_succ case_zero)

Nat.mul_succ_r
: {a : (Nat a)} {b : (Nat b)} (Eq Nat (Nat.mul a (Nat.succ b)) (Nat.add a (Nat.mul a b)) (Nat.mul_succ_r a b))
= [a]
  let motive [self] {b : (Nat b)}
    (Eq Nat (Nat.mul self (Nat.succ b)) (Nat.add self (Nat.mul self b)) (Nat.mul_succ_r self b))
  let case_succ [a] [b]
    (Eq.cong Nat Nat
      (Nat.add b (Nat.mul a (Nat.succ b)))
      (Nat.add a (Nat.add b (Nat.mul a b)))
      (Eq.trans Nat
	(Nat.add b (Nat.mul a (Nat.succ b)))
	(Nat.add b (Nat.add a (Nat.mul a b)))
	(Nat.add a (Nat.add b (Nat.mul a b)))
	(Eq.cong Nat Nat
	  (Nat.mul a (Nat.succ b))
	  (Nat.add a (Nat.mul a b))
	  (Nat.mul_succ_r a b)
	  [x : (Nat x)] (Nat.add b x))
	(Nat.add_swap b a (Nat.mul a b)))
      Nat.succ)
  let case_zero [b]
    (Eq.refl Nat Nat.zero)
  (a motive case_succ case_zero)

Nat.mul_comm
: {a : (Nat a)} {b : (Nat b)} (Eq Nat (Nat.mul a b) (Nat.mul b a) (Nat.mul_comm a b))
= [a]
  let motive [self] {b : (Nat b)}
    (Eq Nat (Nat.mul self b) (Nat.mul b self) (Nat.mul_comm self b))
  let case_succ [a] [b]
    (Eq.trans_r Nat (Nat.add b (Nat.mul a b)) (Nat.add b (Nat.mul b a))
      (Nat.mul b (Nat.succ a))
      (Eq.cong Nat Nat (Nat.mul a b) (Nat.mul b a) (Nat.mul_comm a b) [x : (Nat x)] (Nat.add b x))
      (Nat.mul_succ_r b a))
  let case_zero [b]
    (Eq.sym Nat (Nat.mul b Nat.zero) Nat.zero (Nat.mul_zero_r b))
  (a motive case_succ case_zero)

-- Proof that `(a + b) * c == (a * c) + (b * c)`
Nat.mul_distr_r
: {a : (Nat a)} {b : (Nat b)} {c : (Nat c)}
  (Eq Nat (Nat.mul (Nat.add a b) c) (Nat.add (Nat.mul a c) (Nat.mul b c)) (Nat.mul_distr_r a b c))
= [a]
  let motive [self] {b : (Nat b)} {c : (Nat c)}
    (Eq Nat (Nat.mul (Nat.add self b) c) (Nat.add (Nat.mul self c) (Nat.mul b c)) (Nat.mul_distr_r self b c))
  let case_succ [a] [b] [c]
    (Eq.subst Nat (Nat.add (Nat.mul a c) (Nat.mul b c)) (Nat.mul (Nat.add a b) c)
	(Eq.sym Nat (Nat.mul (Nat.add a b) c) (Nat.add (Nat.mul a c) (Nat.mul b c)) (Nat.mul_distr_r a b c))
	[x : (Nat x)] (Eq Nat (Nat.add c x) (Nat.add (Nat.add c (Nat.mul a c)) (Nat.mul b c)))
	(Nat.add_assoc_r c (Nat.mul a c) (Nat.mul b c)))
   let case_zero [b] [c] (Eq.refl Nat (Nat.mul b c))
   (a motive case_succ case_zero)

-- Natural numbers (Church)

Cat
: (Self Cat)
= [self]
  {P : (Self P)}
  {s : {x : (P x)} (P (s x))}
  {z : (P z)}
  (P (self P s z))

Cat.succ
: {n : (Cat n)} (Cat (Cat.succ n))
= [n] [P] [s] [z]
  (s (n P s z))

Cat.zero
: (Cat Cat.zero)
= [P] [s] [z]
  z

Cat.0 : (Cat Cat.0) = Cat.zero
Cat.1 : (Cat Cat.1) = (Cat.succ Cat.0)
Cat.2 : (Cat Cat.2) = (Cat.succ Cat.1)
Cat.3 : (Cat Cat.3) = (Cat.succ Cat.2)
Cat.4 : (Cat Cat.4) = (Cat.succ Cat.3)
Cat.5 : (Cat Cat.5) = (Cat.succ Cat.4)
Cat.6 : (Cat Cat.6) = (Cat.succ Cat.5)
Cat.7 : (Cat Cat.7) = (Cat.succ Cat.6)
Cat.8 : (Cat Cat.8) = (Cat.succ Cat.7)
Cat.9 : (Cat Cat.9) = (Cat.succ Cat.8)

Cat.add
: {n : (Cat n)} {m : (Cat m)} (Cat (Cat.add n m))
= [n] [m] [P] [s] [z]
  (n P s (m P s z))

Cat.mul
: {n : (Cat n)} {m : (Cat m)} (Cat (Cat.mul n m))
= [n] [m] [P] [s] [z]
  (n P (m P s) z)

Cat.ex
: (Eq Cat Cat.zero Cat.zero (Eq.refl Cat Cat.zero))
= (Eq.refl Cat Cat.zero)

Cat.even
: {n : (Cat n)} (Bool (Cat.even n))
= [n]
  (n
    [n : (Bool n)] (Bool n)
    [n : (Bool n)] (Bool.not n)
    Bool.true)

-- Natural numbers (Parigot)

Rat
: (Self Rat)
= [self]
  {Prop : {self : (Rat self)} {fold : (Prop self fold)} Type}
  {succ : {pred : (Rat pred)} {fold : (Prop pred fold)} (Prop (Rat.succ pred) (succ pred fold))}
  {zero : (Prop Rat.zero zero)}
  (Prop self (self Prop succ zero))

Rat.succ
: {pred : (Rat pred)} (Rat (Rat.succ pred))
= [pred] [Rat] [succ] [zero]
  (succ pred (pred Rat succ zero))

Rat.zero
: (Rat Rat.zero)
= [Rat] [succ] [zero] zero

Rat.0 : (Rat Rat.0) = Rat.zero
Rat.1 : (Rat Rat.1) = (Rat.succ Rat.0)
Rat.2 : (Rat Rat.2) = (Rat.succ Rat.1)
Rat.3 : (Rat Rat.3) = (Rat.succ Rat.2)
Rat.4 : (Rat Rat.4) = (Rat.succ Rat.3)
Rat.5 : (Rat Rat.5) = (Rat.succ Rat.4)
Rat.6 : (Rat Rat.6) = (Rat.succ Rat.5)
Rat.7 : (Rat Rat.7) = (Rat.succ Rat.6)
Rat.8 : (Rat Rat.8) = (Rat.succ Rat.7)
Rat.9 : (Rat Rat.9) = (Rat.succ Rat.8)

Rat.to_cat
: {n : (Rat n)} (Cat (Rat.to_cat n))
= [n] (n
  [self : (Rat self)] [fold : (Cat fold)] (Cat fold)
  [pred : (Rat pred)] [fold : (Cat fold)] (Cat.succ fold)
  Cat.zero)

Rat.id
: {n : (Rat n)} (Rat (Rat.id n))
= [n] (n
  [self : (Rat self)] [fold : (Rat fold)] (Rat fold)
  [pred : (Rat pred)] [fold : (Rat fold)] (Rat.succ (Rat.succ (Rat.succ fold)))
  Rat.zero)

Rat.add_n_zero
: {n : (Rat n)} (Eq Rat (Rat.add n Rat.zero) n (Rat.add_n_zero n))
= [n]
  let motive [self : (Rat self)] [fold : (Eq Rat (Rat.add self Rat.zero) self fold)]
    (Eq Rat (Rat.add self Rat.zero) self fold)
  let case_succ [pred : (Rat pred)] [fold : (Eq Rat (Rat.add pred Rat.zero) pred fold)]
    (Eq.cong Rat Rat (Rat.add pred Rat.zero) pred (Rat.add_n_zero pred) Rat.succ)
  let case_zero
    (Eq.refl Rat Rat.zero)
  (n motive case_succ case_zero)

Rat.add
: {n : (Rat n)} {m : (Rat m)} (Rat (Rat.add n m))
= [n] [m] (n
  [n : (Rat n)] [r : (Rat r)] (Rat r)
  [n : (Rat n)] [r : (Rat r)] (Rat.succ r)
  m)

-- Equality

Eq
: {T    : (Self T)}
  {a    : (T a)}
  {b    : (T b)}
  {self : (Eq T a b self)}
  Type
= [T] [a] [b] [self]
  {Prop : {b : (T b)} {self : (Eq T a b self)} Type}
  {refl : (Prop a (Eq.refl T a))}
  (Prop b self)

Eq.refl
: {T : (Self T)}
  {a : (T a)}
  (Eq T a a (Eq.refl T a))
= [T] [a] [Prop] [refl]
  refl

Eq.sym
: {T : {self : (T self)} Type}
  {a : (T a)}
  {b : (T b)}
  {e : (Eq T a b e)}
  (Eq T b a (Eq.sym T a b e))
= [T] [a] [b] [e]
  (e [b] [self] (Eq T b a (Eq.sym T a b self))
    (Eq.refl T a))

Eq.cong
: {A : {self : (A self)} Type}
  {B : {self : (B self)} Type}
  {a : (A a)}
  {b : (A b)}
  {e : (Eq A a b e)}
  {f : {a : (A a)} (B (f a))}
  (Eq B (f a) (f b) (Eq.cong A B a b e f))
= [A] [B] [a] [b] [e] [f]
  (e [b] [self] (Eq B (f a) (f b) (Eq.cong A B a b self f))
    (Eq.refl B (f a)))

Eq.subst
: {T : (Self T)}
  {a : (T a)}
  {b : (T b)}
  {e : (Eq T a b e)}
  {P : {a : (T a)} (Self (P a))}
  {x : (P a x)}
  (P b (Eq.subst T a b e P x))
= [T] [a] [b] [e] [P] [x]
  (e [b] [self] (P b (Eq.subst T a b self P x)) x)

-- Transitivity of equality: a proof that `a == b` and `b == c` implies `a == c` (and all other permutations)
Eq.trans
: {T : {self : (T self)} Type}
  {a : (T a)}
  {b : (T b)}
  {c : (T c)}
  {e1 : (Eq T a b e1)}
  {e2 : (Eq T b c e2)}
  (Eq T a c (Eq.trans T a b c e1 e2))
= [T] [a] [b] [c] [e1]
  (e1 [b] [self] {e2 : (Eq T b c e2)} (Eq T a c (Eq.trans T a b c self e2))
    [e2] e2)

Eq.trans_r
: {T : {self : (T self)} Type}
  {a : (T a)}
  {b : (T b)}
  {c : (T c)}
  {e1 : (Eq T a b e1)}
  {e2 : (Eq T c b e2)}
  (Eq T a c (Eq.trans_r T a b c e1 e2))
= [T] [a] [b] [c] [e1]
  (e1 [b] [self] {e2 : (Eq T c b e2)} (Eq T a c (Eq.trans_r T a b c self e2))
    [e2] (Eq.sym T c a e2))

Eq.r_trans
: {T : {self : (T self)} Type}
  {a : (T a)}
  {b : (T b)}
  {c : (T c)}
  {e1 : (Eq T b a e1)}
  {e2 : (Eq T b c e2)}
  (Eq T a c (Eq.r_trans T a b c e1 e2))
= [T] [a] [b] [c] [e1]
  (e1 [a] [self] {e2 : (Eq T b c e2)} (Eq T a c (Eq.r_trans T a b c self e2))
    [e2] e2)

Eq.r_trans_r
: {T : {self : (T self)} Type}
  {a : (T a)}
  {b : (T b)}
  {c : (T c)}
  {e1 : (Eq T b a e1)}
  {e2 : (Eq T c b e2)}
  (Eq T a c (Eq.r_trans_r T a b c e1 e2))
= [T] [a] [b] [c] [e1]
  (e1 [a] [self] {e2 : (Eq T c b e2)} (Eq T a c (Eq.r_trans_r T a b c self e2))
    [e2] (Eq.sym T c b e2))

-- Binary

Bin
: (Self Bin)
= [self]
  {Prop : (Self Bin)}
  {O    : {pred : (Bin pred)} (Prop (Bin.O pred))}
  {I    : {pred : (Bin pred)} (Prop (Bin.I pred))}
  {E    : (Prop Bin.E)}
  (Prop self)

Bin.O
: {pred : (Bin pred)}
  (Bin (Bin.O pred))
= [pred] [Prop] [O] [I] [E]
  (O pred)

Bin.I
: {pred : (Bin pred)}
  (Bin (Bin.I pred))
= [pred] [Prop] [O] [I] [E]
  (I pred)

Bin.E
: (Bin Bin.E)
= [Prop] [O] [I] [E]
  E

Bin.inc
: {x : (Bin x)}
  (Bin (Bin.inc x))
= [xs]
  (xs [self : (Bin self)] (Bin (Bin.inc self))
    [pred] (Bin.I pred)
    [pred] (Bin.O (Bin.inc pred))
    Bin.E)

-- Dependent pairs

Sigma
: {A : (Self A)}
  {B : {x : (A x)} (Self (B x))}
  {self : (Sigma A B self)}
  Type
= [A] [B] [self]
  {Prop : {self : (Sigma A B self)} Type}
  {new  : {a : (A a)} {b : (B a b)} (Prop (Sigma.new A B a b))}
  (Prop self)

Sigma.new
: {A : (Self A)}
  {B : {x : (A x)} (Self (B x))}
  {a : (A a)}
  {b : (B a b)}
  (Sigma A B (Sigma.new A B a b))
= [A] [B] [a] [b] [Prop] [new]
  (new a b)

Sigma.fst
: {A : (Self A)}
  {B : {x : (A x)} (Self (B x))}
  {sigma : (Sigma A B sigma)}
  (A (Sigma.fst A B sigma))
= [A] [B] [sigma]
  (sigma
    [self] (A (Sigma.fst A B self))
    [a] [b] a)

Sigma.snd
: {A : (Self A)}
  {B : {x : (A x)} (Self (B x))}
  {sigma : (Sigma A B sigma)}
  (B (Sigma.fst A B sigma) (Sigma.snd A B sigma))
= [A] [B] [sigma]
  (sigma
    [self] (B (Sigma.fst A B self) (Sigma.snd A B self))
    [a] [b] b)

Sigma.example
= (Sigma.new Nat [x : (Nat x)](Eq Nat x x) Nat.3 (Eq.refl Nat Nat.3))

main
= Nat.mul_distr_r