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 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 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$.
It's also interesting to note that $\mathbb N$ belongs to a class of inductive types, which means the eliminator has a specific form.
$\newcommand{\mc}{\mathcal}$
Indeed, for an inductive type defined by an endofunctor $F:\mc C\to\mc C$ (where $\mc C$ is the category of types) (in the case of $\mathbb N$, $F(X) := X\times (X\to X)$), the inductive type is defined to be the initial algebra for $F$. If $A$ is initial for $F$, this briefly means that for every other type $X$, there is a unique map of algebras $F(A)\to F(X)$. This map is the eliminator for $A$.
