let sucf : ℕ → ℕ
  ≔ λn. suc n

let add : ℕ → ℕ → ℕ
  ≔ ℕ-ind (λ_. ℕ → ℕ) (λn.n) (λn.λan.λm. suc (an m))

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 ℕ ℕ sucf 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 ℕ ℕ sucf (add (add n m) p) (add n (add m p)) (pn m p))