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 ℕ