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))