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.