自然数型

形成：$\vdash\mathbb{N}\ \mathsf{type}$。導入：$\vdash0:\mathbb{N}$、$n:\mathbb{N}\vdash\mathrm{succ}(n):\mathbb{N}$。

除去：型族 $\Gamma,n{:}\mathbb{N}\vdash C(n)\ \mathsf{type}$、$\Gamma\vdash c_0:C(0)$、$\Gamma\vdash c_s:\Pi_{(n:\mathbb{N})}C(n)\to C(\mathrm{succ}(n))$ から、$\Gamma,n{:}\mathbb{N}\vdash\mathrm{ind}(c_0,c_s,n):C(n)$。

計算：$\mathrm{ind}(c_0,c_s,0)\equiv c_0$、$\mathrm{ind}(c_0,c_s,\mathrm{succ}(n))\equiv c_s\,n\,\mathrm{ind}(c_0,c_s,n)$。