I'm familiar with elimination rules from logic. Elimination rules, as a rule, get rid of a connective and have conclusions that are structurally smaller than their premises.

$$ \frac{A \land B}{A} \;\; \text{and} \;\; \frac{A \land B}{B} \;\; \text{are conjunction elimination} $$

And from type theory; here's an example from the simply typed lambda calculus (henceforth STLC).

$$ \frac{\Gamma \vdash e_1 : A \to B \;\; \text{and} \;\; \Gamma \vdash e_2 : A}{\Gamma \vdash e_1(e_2) : B} \;\; \text{is function elimination} $$

In the context above, I'm used to $\square(\square)$ being called an elimination form similar to $\pi_1$ and $\pi_2$ for binary products. My understanding is that these things are forms because they're part of the inductive definition of what a term is.

However, these things are not really first-class values in STLC. Function application, $\pi_1$, and $\pi_2$ cannot be given types without some kind of polymorphism, which STLC does not have.

Eliminators (assuming they're a distinct thing from an elimination form) appear in this question and in this answer to a question I asked previously.

From the latter example, we have the definition of $\mathbb{N}$ below. This definition sort of makes sense. $\Pi$-types are like a universal quantifier. A type headed by a $\Pi$-type is inhabited if and only if every instantiation of it is inhabited. As a type, intuitively I think of $\Pi \alpha : \kappa \mathop. \varphi(\cdots)$ as returning the least type satisfying $\varphi(\cdots)$ (according to some ordering that I don't really understand).

$$ \mathbb{N} \;\;\text{is defined as}\;\; \bigg(\Pi (N : *) \mathop. \Pi (A : *) \mathop. A \to (N \to A \to A) \to (N \to A)\bigg) : * $$

By leveraging the fact that $A \times B \to C$ is isomorphic to $A \to B \to C$ we can rewrite the matrix (the part of the type with the $\Pi$-s stripped, named by analogy with wffs in FOL) in the following way.

$$ f : A \times (N \times A \to A) \times N \to A $$

The only implementation of $f$ that really makes sense here is:

$$f(x, g, n) = g(n, f(x, g, n)) $$

The idea being that we're going to use the fact that this function must terminate against $N$, so to speak. I think this amounts to saying that the natural numbers are, in an extremely loose intuitive sense, the least thing you can induct on.

We can cook up other terms with the same type though, such as

$$ f''(x, g, n) = x $$

So, it's not clear to me what an eliminator is ... or how we know we're getting one when try to use them in a definition.