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