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%)).