# A.1.6 Natural numbers

The type of natural numbers is obtained by introducing primitive constants $\mathbb{N}$, $0$, and $\mathsf{succ}$ with the following rules:

• $\mathbb{N}:\mathcal{U}_{0}$,

• $0:\mathbb{N}$,

• $\mathsf{succ}:\mathbb{N}\rightarrow\mathbb{N}$.

Furthermore, we can define functions by primitive recursion. If we have $C:\mathbb{N}\rightarrow\mathcal{U}_{k}$ we can introduce a defined constant $f:\mathchoice{{\textstyle\prod_{(x:\mathbb{N})}}}{\prod_{(x:\mathbb{N})}}{% \prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}C(x)$ whenever we have

 $\displaystyle d$ $\displaystyle:C(0)$ $\displaystyle e$ $\displaystyle:\mathchoice{{\textstyle\prod_{(x:\mathbb{N})}}}{\prod_{(x:% \mathbb{N})}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}(C(x)\rightarrow C% (\mathsf{succ}(x)))$

with the defining equations

 $f(0):\!\!\equiv d\qquad\text{and}\qquad f(\mathsf{succ}(x)):\!\!\equiv e(x,f(x% )).$
Title A.1.6 Natural numbers
\metatable