Recursor

For an Inductive Type. Construct a fixed type that doesn’t change with recursion.

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}$.

See also

Eliminator