# 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