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}}& :(A:Set)\to A\to (A\to A)\to \mathbb{N}\to A\\ {\mathrm{elim}}_{\mathbb{N}}& :(A:\mathbb{N}\to Set)\to (A0)\to ((n:\mathbb{N})\to An\to A(n^{\prime }))\to (n:\mathbb{N})\to 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