A.1.6 Natural numbers

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

• $\mathbb{N}:{𝒰}_0$,

• $0:\mathbb{N}$,

• $\mathrm{𝗌𝗎𝖼𝖼}:\mathbb{N}\to \mathbb{N}$.

Furthermore, we can define functions by primitive recursion. If we have$C:\mathbb{N}\to {𝒰}_k$ we can introduce a defined constant $f:{\prod }_{(x:\mathbb{N})}C(x)$ whenever we have

$d$$:C(0)$

$e$$:{\prod }_{(x:\mathbb{N})}(C(x)\to C(\mathrm{𝗌𝗎𝖼𝖼}(x)))$

with the defining equations

$$f(0):\equiv d\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}f(\mathrm{𝗌𝗎𝖼𝖼}(x)):\equiv e(x,f(x)).$$