Fin

Definition

$\mathrm{Fin}:\mathbb{N}\to \mathcal{U}$ is defined as the initial algebra of the following indexed signature:

$$\frac{n:\mathbb{N}}{\mathrm{fzero}:\mathrm{Fin}(\mathrm{suc}n)}\frac{n:\mathbb{N}a:\mathrm{Fin}n}{\mathrm{fsuc}a:\mathrm{Fin}(\mathrm{suc}n)}$$

Remarks

Fin is an indexed inductive type, thus can be represented using indexed W-types.