24 lines
932 B
Plaintext
24 lines
932 B
Plaintext
let add : ℕ → ℕ → ℕ
|
||
≔ ℕ-ind (λ_. ℕ → ℕ) (λn.n) (λn.λan.λm. suc (an m))
|
||
|
||
let add_test : Id ℕ (add 2 2) 4
|
||
≔ refl ℕ 4
|
||
|
||
let add_id_l : Π (n : ℕ) Id ℕ n (add 0 n)
|
||
≔ λn. refl ℕ n
|
||
|
||
let ap : Π (A : Type) Π (B : Type) Π (f : A → B)
|
||
Π (x : A) Π (y : A) Id A x y → Id B (f x) (f y)
|
||
≔ λA.λB.λf.λx.λy. J A x y (λa.λb.λ_. Id B (f a) (f b)) (refl B (f x))
|
||
|
||
let add_id_r : Π (n : ℕ) Id ℕ n (add n 0)
|
||
≔ ℕ-ind (λn. Id ℕ n (add n 0))
|
||
(refl ℕ 0)
|
||
(λn.λp. ap ℕ ℕ (λm. suc m) n (add n 0) p)
|
||
|
||
let add_assoc : Π (n : ℕ) Π (m : ℕ) Π (p : ℕ)
|
||
Id ℕ (add (add n m) p) (add n (add m p))
|
||
≔ ℕ-ind (λn. Π (m : ℕ) Π (p : ℕ) Id ℕ (add (add n m) p) (add n (add m p)))
|
||
(λm.λp. refl ℕ (add m p))
|
||
(λn.λpn.λm.λp. ap ℕ ℕ (λm. suc m) (add (add n m) p) (add n (add m p)) (pn m p))
|