Eliminator

For an Inductive Type. Constructs a dependent type that changes as you recurse.

Discussion

For example ($\mathbb{N}$):

$$\begin{array}{rl}{\mathrm{rec}}_{\mathbb{N}}& :\prod _{A:Set}A\to (A\to A)\to \mathbb{N}\to A\\ {\mathrm{elim}}_{\mathbb{N}}& :\prod _{A:\mathbb{N}\to Set}(A0)\to (\prod _{n:\mathbb{N}}An\to A(n^{\prime }))\to \prod _{n:\mathbb{N}}An\end{array}$$

Here $A$ is called the motive. The methods are the are the consumers that align with the constructors. In the eliminator, $A$ is an indexed family indexed by $\mathbb{N}$.

Link to original

See also

Recursor