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 β„•