A.2.9 The natural number type

We give the rules for natural numbers, following §1.9 (http://planetmath.org/19thenaturalnumbers).

*[right=$\mathbb{N}$-form] Γ $\mathrm{𝖼𝗍𝗑}$ Γ ⊢$\mathbb{N}$ : $𝒰$ _i *[right=$\mathbb{N}$-intro${}_{\mathrm{1}}$] Γ $\mathrm{𝖼𝗍𝗑}$ Γ ⊢0 : $\mathbb{N}$ *[right=$\mathbb{N}$-intro${}_{\mathrm{2}}$] Γ ⊢n : $\mathbb{N}$ Γ ⊢succ(n) : $\mathbb{N}$ *[right=$\mathbb{N}$-elim] Γ,x : $\mathbb{N}$ ⊢C : $𝒰$ _i
Γ ⊢c_0 : C[0/x]
Γ,x : $\mathbb{N}$,y : C ⊢c_s : C[succ(x)/x]
Γ ⊢n : $\mathbb{N}$ Γ ⊢ind_$\mathbb{N}$(x.C,c_0,x.y.c_s,n) : C[n/x] *[right=$\mathbb{N}$-comp${}_{\mathrm{1}}$] Γ,x : $\mathbb{N}$ ⊢C : $𝒰$ _i
Γ ⊢c_0 : C[0/x]
Γ,x : $\mathbb{N}$,y : C ⊢c_s : C[succ(x)/x] Γ ⊢ind_$\mathbb{N}$(x.C,c_0,x.y.c_s,0) ≡c_0 : C[0/x] *[right=$\mathbb{N}$-comp${}_{\mathrm{2}}$] Γ,x : $\mathbb{N}$ ⊢C : $𝒰$ _i
Γ ⊢c_0 : C[0/x]
Γ,x : $\mathbb{N}$,y : C ⊢c_s : C[succ(x)/x]
Γ ⊢n : $\mathbb{N}$ Γ⊢ ind $\mathbb{N}$ (x.C,c 0 ,x.y.c s ,succ(n))  ≡c s [n,ind $\mathbb{N}$ (x.C,c 0 ,x.y.c s ,n)/x,y] : C[succ(n)/x] In ${\mathrm{𝗂𝗇𝖽}}_{\mathbb{N}}$, $x$ is bound in $C$, and $x$ and $y$ are bound in $c_s$.

Other inductively defined types follow the same general scheme.

Title	A.2.9 The natural number type