test.input

id :: Forall (A : Type). A -> A;;
id := \A. \x. x;;

id_impli :: Forall {A : Type}. A -> A;;
id_impli := \x. x;;

id_nat :: Nat -> Nat;;
id_nat := id Nat;;

eq_refl :: Forall (A : Type). Forall (x : A). x = x;;
eq_refl := \A. \x. Refl A x;;

two :: Nat;;
two := Succ (Succ Zero);;

three :: Nat;;
three := Succ two;;

succ :: Nat -> Nat;;
succ := \x. Succ x;;

plus :: Nat -> Nat -> Nat;;
plus := \x. \y. nat_elim (\_. Nat) y (\_. \h. Succ h) x;;

test_plus_1 :: Forall (x : Nat). plus Zero (succ x) = (succ x);;
test_plus_1 := \x. Refl Nat (Succ x);;

f_eq :: Forall (A : Type). Forall (B : Type). Forall (x : A). Forall (y : A). Forall (f : Forall (x : A). B). Forall (eq : (x = y)). (f x) = (f y);;
f_eq := \A. \B. \x. \y. \f. \eqf.
            eq_elim A
                    (\u. \v. (f u) = (f v))
                    (\w. Refl B (f w))
                    eqf;;

eq_trans :: Forall (A : Type). Forall (a : A). Forall (b : A). Forall (c : A). a = b -> b = c -> a = c;;
eq_trans := \A. \a. \b. \c.\Eab.
            eq_elim A (\u. \v. v = c -> u = c)
                      (\w : A. id (w = c))
                      Eab;;

eq_sym :: Forall (A : Type). Forall (a : A). Forall (b : A). a = b -> b = a;;
eq_sym := \A. \a. \b. \eq.
            eq_elim A (\u.\v. v = u)
                      (\w. Refl A w)
                      eq;;

eq_sym_again :: Forall (A : Type). Forall (a : A). Forall (b : A). Forall (eq : (a = b)). b = a;;
eq_sym_again := \A. \x. \y. \eq. eq_sym A x y eq;;

two_eq_two :: two = (plus (Succ Zero) (Succ Zero));;
two_eq_two := Refl Nat two;;

test_plus :: Forall (x : Nat). (plus Zero x) = x;;
test_plus := \n. Refl Nat n;;

plus_Z :: Forall (x : Nat). (plus x Zero) = x;;
plus_Z := \x. nat_elim (\z. (plus z Zero) = z)
                            (Refl Nat Zero)
                            (\n. \h. f_eq Nat Nat (plus n Zero) n succ h)
                            x;;

plus_nSm :: Forall (x : Nat). Forall (y : Nat). (plus x (succ y)) = (succ (plus x y));;
plus_nSm := \x. \y.
            nat_elim (\z. (plus z (succ y)) = (succ (plus z y)))
                     (f_eq Nat Nat y y succ (Refl Nat y))
                     (\n. \IH : ((plus n (succ y)) = (succ (plus y n))). f_eq Nat Nat (plus n (Succ y)) (Succ (plus n y)) succ IH)
                     x;;

plus_comm :: Forall (x : Nat). Forall (y : Nat). (plus x y) = (plus y x);;
plus_comm := \x. \y.
            nat_elim (\z. (plus z y) = (plus y z))
                     (eq_sym Nat (plus y Zero) y (plus_Z y))
                     (\n. \IH.
                     eq_trans Nat 
                            (succ (plus n y))
                            (succ (plus y n))
                            (plus y (succ n))
                            (f_eq Nat Nat (plus n y) (plus y n) succ IH) 
                            (eq_sym Nat (plus y (succ n)) (succ (plus y n)) (plus_nSm y n)))
                     x;;

times_two :: Nat -> Nat;;
times_two := \x : Nat. plus x x;;

times :: Nat -> Nat -> Nat;;
times := \x : Nat. \y : Nat.
            nat_elim (\_. Nat)
                     Zero
                     (\n : Nat. \rec : Nat. plus rec y)
                     x;;

test_times :: Forall (x : Nat). times two x = times_two x;;
test_times := \x : Nat. Refl Nat (times two x);;

apply :: Forall (A : Type). Forall (B : Type). (A -> B) -> A -> B;;
apply := \A. \B. \f. \x. f x;;

dependent_apply :: Forall (A : Type). Forall (B : A -> Type). Forall (x : A). (A -> (B x)) -> B x;;
dependent_apply := \A. \B. \x. \f. f x;;

# Postulate
my_nat_elim :: Forall (goal : (Nat -> Type)). goal Zero -> Forall (ind : (Forall (n : Nat). Forall (IH : goal n). goal (Succ n))). Forall (x : Nat). goal x;;

plus_Z_again :: Forall (x : Nat). (plus x Zero) = x;;
plus_Z_again := \x. my_nat_elim
                    (\z. (plus z Zero) = z)
                    (Refl Nat Zero)
                    (\n. \h. f_eq Nat Nat (plus n Zero) n succ h)
                    x;;

six :: Nat;;
six := plus (plus two two) two;;

sum :: Nat -> Nat;;
sum := \x. nat_elim (\_. Nat) Zero (\n : Nat. \rec : Nat. plus n rec) (Succ x);;

test_plus_2 :: six = (sum three);;
test_plus_2 := Refl Nat six;;

test_sum_prop :: (sum (times_two two)) = times two (Succ (times_two two));;
test_sum_prop := Refl Nat (sum (times_two two));;

Normalize (sum three);;

or_nat :: Nat | Nat;;
or_nat := inl Zero;;

or_id :: (Nat -> Nat) | (Forall (A : Type). A -> A);;
or_id := inr id;;

Normalize (id_nat (sum six));;

test_id_nat :: (id_nat (sum six)) = sum six;;
test_id_nat := Refl Nat (sum six);;

test_pair :: Nat * Nat;;
test_pair := < Zero , Zero >;;

Normalize (Fst test_pair);;

# CH Correspondence
case_sum :: Forall (A : Type). Forall (B : Type). Forall (C : Type). (A -> C) -> (B -> C) -> (A | B) -> C;;
case_sum := \A. \B. \C. \fac. \fbc. \ab.
            sum_elim (\_. C) (\l. fac l) (\r. fbc r) ab;;

case_prod :: Forall {A : Type}. Forall {B : Type}. Forall {C : Type}. (A -> C) -> (B -> C) -> (A * B) -> C;;
case_prod := \ac. \_. \ab. ac (Fst ab);;

weaken :: Forall (A : Type). Forall (B : Type). Forall (C : Type). (C -> A) -> (C -> (A | B));;
weaken := \A. \B. \C. \fca. \c. inl (fca c);;

prod_weaken :: Forall (A : Type). Forall (B : Type). (A * B) -> (A | B);;
prod_weaken := \A. \B. \prod. inl (Fst prod);;

f_comp :: Forall (A : Type). Forall (B : Type). Forall (C : Type). (B -> C) -> (A -> B) -> (A -> C);;
f_comp := \A. \B. \C. \bc. \ab. (\x. bc (ab x));;

dependent_comp :: Forall (A : Type).
                  Forall (B : A -> Type).
                  Forall (C : (Forall (x : A). B x -> Type)).
                  Forall (f : (Forall (x : A). Forall (y : (B x)). C x y)).
                  Forall (g : Forall (x : A). B x).
                  Forall (x : A). C x (g x);;
dependent_comp := \A. \B. \C. \f. \g. \x : A. f x (g x);;

proj_1 :: Forall (A : Type). Forall (B : Type). Forall (x : A * B). A;;
proj_1 := \A. \B. \p. Fst p;;

proj_2 :: Forall (A : Type). Forall (B : Type). Forall (x : A * B). B;;
proj_2 := \A. \B. \p. Snd p;;

inj_1 :: Forall (A : Type). Forall (B : Type). Forall (x : A). A | B;;
inj_1 := \A. \B. \x. inl x;;

inj_2 :: Forall (A : Type). Forall (B : Type). Forall (x : B). A | B;;
inj_2 := \A. \B. \x. inr x;;

arr_distrib :: Forall (A : Type). Forall (B : Type). Forall (C : Type). ((A | B) -> C) -> ((A -> C) * (B -> C));;
arr_distrib := \A. \B. \C. \f. < f_comp A (A | B) C f (inj_1 A B) , f_comp B (A | B) C f (inj_2 A B) >;;

inj_1_impli :: Forall {A : Type}. Forall {B : Type}. Forall (x : A). A | B;;
inj_1_impli := \x. inl x;;

inj_2_impli :: Forall {A : Type}. Forall {B : Type}. Forall (x : B). A | B;;
inj_2_impli := \x. inr x;;

f_comp_impli :: Forall {A : Type}. Forall {B : Type}. Forall {C : Type}. (B -> C) -> (A -> B) -> (A -> C);;
f_comp_impli := \bc. \ab. (\x. bc (ab x));;

arr_distrib_impli :: Forall {A : Type}. Forall {B : Type}. Forall {C : Type}. ((A | B) -> C) -> ((A -> C) * (B -> C));;
arr_distrib_impli := \f. < f_comp_impli f inj_1_impli , f_comp_impli f inj_2_impli >;;

Normalize (inj_1_impli Zero);;

refl :: Forall {A : Type}. Forall {x : A}. x = x;;
refl := \{A}. \{x}. Refl A x;;

eq_number :: six = six;;
eq_number := refl;;

eq_trans_impli :: Forall {A : Type}. Forall {a : A}. Forall {b : A}. Forall {c : A}. a = b -> b = c -> a = c;;
eq_trans_impli := \{A}. \{a}. \{b}. \{c}. \Eab.
                    eq_elim A (\u. \v. v = c -> u = c)
                      (\w : A. id_impli)
                      Eab;;

eq_sym_impli :: Forall {A : Type}. Forall {a : A}. Forall {b : A}. a = b -> b = a;;
eq_sym_impli := \{A}. \{a}. \{b}. \eq.
                eq_elim A (\u.\v. v = u)
                        (\w. refl)
                        eq;;

f_eq_impli :: Forall {A : Type}. Forall {B : Type}. Forall {x : A}. Forall {y : A}. Forall (f : A -> B). x = y -> (f x) = (f y);;
f_eq_impli := \{A}. \{B}. \{x}. \{y}. \f. \eqf.
                eq_elim A
                    (\u. \v. (f u) = (f v))
                    (\w. refl)
                    eqf;;

plus_Z_simpler :: Forall (x : Nat). (plus x Zero) = x;;
plus_Z_simpler := \x. nat_elim (\z. (plus z Zero) = z)
                            refl
                            (\n. \h. f_eq_impli succ h)
                            x;;

plus_nSm_simpler :: Forall (x : Nat). Forall (y : Nat). (plus x (succ y)) = (succ (plus x y));;
plus_nSm_simpler := \x. \y.
            nat_elim (\z. (plus z (succ y)) = (succ (plus z y)))
                     (f_eq_impli succ refl)
                     (\n. \IH : ((plus n (succ y)) = (succ (plus y n))). f_eq_impli succ IH)
                     x;;

plus_comm_simpler :: Forall (x : Nat). Forall (y : Nat). (plus x y) = (plus y x);;
plus_comm_simpler := \x. \y.
                    nat_elim (\z. (plus z y) = (plus y z))
                            (eq_sym_impli (plus_Z y))
                            (\n. \IH.
                            eq_trans_impli
                                    (f_eq_impli succ IH) 
                                    (eq_sym_impli (plus_nSm y n)))
                            x;;

uip :: Forall {A : Type}. Forall {x : A}. Forall {y : A}. Forall {p : x = y}. Forall {q : x = y}. p = q;;
uip := refl;;

Normalize (id_impli six);;

application :: Nat;;
application := succ two;;

Normalize application;;

trivial_prop :: Forall {x : Nat}. Forall {y : Nat}. x = y -> succ x = succ y;;
trivial_prop := \{x}. \{y}. \eq_xy. eq_elim Nat (\n. \m. succ n = succ m) (\w. refl) eq_xy;;

Data Natural : Type where
      Z : Natural
    | S : Natural -> Natural;;

Data NatTree : Type where
      Leaf   : (Natural -> NatTree)
    | Branch : (Natural -> NatTree -> NatTree -> NatTree);;

# NaturalElim :   Forall (n : Natural).
#                 Forall (goal : Natural -> Type).
#                 Forall (base : goal Z).
#                 Forall (x : Natural). goal x -> goal (S x).
#                 goal n;;