The role of constructors and eliminators can be understood through category theory. For every type former (for example $A\times B$, $A+B$, $A^B$, $\mathbb N$, etc...) we can ask - How can we construct a morphism *into* this type? - How can we construct a morphism *out* of this type? We might as well call the morphisms into the type *constructors* and morphisms out of the type as *eliminators*. The product type, for example, has the following universal property: > Given $P,Q$, there exists morphisms $\pi_1 : P\times Q\to P$, $\pi_2 : P\times Q\to Q$, such that for every object $R$, and morphisms $p : R\to P$, $q:R\to Q$ such that $\pi_1\circ p = \pi_2\circ q$, there exists a unique morphism $\langle p,q\rangle : R\to P\times Q$ such that $\langle p,q\rangle\circ \pi_1 = p$ and $\langle p,q\rangle\circ\pi_2 = q$. From this, we see that the eliminators are $$\pi_1 : P\times Q\to P\\\pi_2 : P\times Q\to Q$$ and the only constructor is $$\frac{p : R\to P\quad q : R\to Q}{\langle p,q\rangle : R\to P\times Q}.$$ Similarly, the [universal property of the natural numbers](https://en.wikipedia.org/wiki/Natural_numbers_object) gives constructors $$z : 1\to \mathbb N\\ s : \mathbb N\to \mathbb N$$ and eliminators $$\frac{q : 1\to A\quad f : A\to A}{\text{rec}(q,f) : \mathbb N\to A}$$ Note that this is slightly different from require $f : \mathbb N\to A\to A$, but this is an equivalent, and often more convenient presentation. So there is no reason why we can't have more than one eliminator, or that constructors/eliminators can't be more complicated. As a final example, [function types](https://en.wikipedia.org/wiki/Exponential_object) have constructor $$\frac{f : A\to B}{\lambda f : B^A}$$ and eliminator $$\text{eval} : B^A\times A\to B,$$ where the only way to eliminate something of type $B^A$ is to pair it with something of type $A$.