A.1.5 The finite types

We introduce primitive constants $\star$ , $\mathbf{0}$ , $\mathbf{1}$ , satisfying the following rules:

•

$\mathbf{0}:\mathcal{U}_{0}$ , $\mathbf{1}:\mathcal{U}_{0}$
•

$\star:\mathbf{1}$

Given $C:\mathbf{0}\rightarrow\mathcal{U}_{n}$ we can introduce a defined constant $f:\mathchoice{{\textstyle\prod_{(x:\mathbf{0})}}}{\prod_{(x:\mathbf{0})}}{% \prod_{(x:\mathbf{0})}}{\prod_{(x:\mathbf{0})}}C(x)$ , with no defining equations.

Given $C:\mathbf{1}\rightarrow\mathcal{U}_{n}$ and $d:C(\star)$ we can introduce a defined constant $f:\mathchoice{{\textstyle\prod_{(x:\mathbf{1})}}}{\prod_{(x:\mathbf{1})}}{% \prod_{(x:\mathbf{1})}}{\prod_{(x:\mathbf{1})}}C(x)$ , with defining equation $f(\star):\!\!\equiv d$ .

Title	A.1.5 The finite types
\metatable