# A.2.9 The natural number type

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

{mathparpagebreakable}\inferrule

*[right=$\mathbb{N}$-form] ΞΒ $\mathsf{ctx}$ Ξ β’$\mathbb{N}$ : $\mathcal{U}$ _i \inferrule*[right=$\mathbb{N}$-intro${}_{1}$] ΞΒ $\mathsf{ctx}$ Ξ β’0 : $\mathbb{N}$ \inferrule*[right=$\mathbb{N}$-intro${}_{2}$] Ξ β’n : $\mathbb{N}$ Ξ β’succ(n) : $\mathbb{N}$ \inferrule*[right=$\mathbb{N}$-elim] Ξ,x : $\mathbb{N}$ β’C : $\mathcal{U}$ _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] \inferrule*[right=$\mathbb{N}$-comp${}_{1}$] Ξ,x : $\mathbb{N}$ β’C : $\mathcal{U}$ _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] \inferrule*[right=$\mathbb{N}$-comp${}_{2}$] Ξ,x : $\mathbb{N}$ β’C : $\mathcal{U}$ _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 $\mathsf{ind}_{\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
\metatable