NAT

NATURAL NUMBERS

Pointed Unary System is a category with the terminal object and a carrier nat having morphism . The initial object of is called Natural Number Object and models Peano axiom set.

In type theory type could be expressed as

def β := W (x : π), indβ (Ξ» (_ : π), U) π π x def β-ctor := indβ (Ξ» (_ : π), U) π π

Constructors

Type provides two way of creating numbers: by and constructors.

def zero : β := sup π β-ctor 0β (indβ β) def succ (n : β) : β := sup π β-ctor 1β (Ξ» (x : π), n) 

Eliminators

The induction principle is derivable in CCHM with W-types:

def β-ind (C : β β U) (z : C zero) (s : Ξ  (n : β), C n β C (succ n)) : Ξ  (n : β), C n := indα΅ π β-ctor C (indβ (Ξ» (x : π), Ξ  (f : β-ctor x β β), (Ξ  (b : β-ctor x), C (f b)) β C (sup π β-ctor x f)) (Ξ» (f : π β β) (g : Ξ  (x : π), C (f x)), πβΆβ C f z) (Ξ» (f : π β β) (g : Ξ  (x : π), C (f x)), πβΆβ C f (s (f β) (g β)))) 

Non-dependent versions:

def β-rec (C : U) (z : C) (s : β β C β C) : β β C := β-ind (Ξ» (_ : β), C) z s def β-iter (C : U) (z : C) (s : C β C) : β β C := β-rec C z (Ξ» (_ : β), s) def β-case (C : U) (z s : C) : β β C := β-iter C z (Ξ» (_ : C), s) 

Transformations

def plus : β β β β β := β-iter (β β β) (idfun β) (β β β β succ) def mult : β β β β β := β-rec (β β β) (Ξ» (_: β), zero) (Ξ» (_: β) (x: β β β) (m: β), plus m (x m)) 

Theorems

def add_zero (n : β) : Path β (add zero n) n def add_suc (a : β) (n : β) : Path β (add (suc a) n) (suc (add a n)) def add_comm (a : β) (n : β) : Path β (add a n) (add n a) def assocAdd (a b : β) (c : β) : Path β (add a (add b c)) (add (add a b) c) def sucInj (n m : β) (p : Path β (suc n) (suc m)) : Path β n m def add_comm3 (a b c : nat) : Path β (add a (add b c)) (add c (add b a)) def caseNat (A : U) (z s : A) : β -> A def natDec (n m : β) : dec (Path β n m) def natSet : isSet β