What is an eliminator? Specifically, what is it in the context of a $\Pi$-type ... such as the one defining the natural numbers quoted from [an answer on this site](https://proofassistants.stackexchange.com/a/327).

What follows is my attempt to make sense of that answer.

-------------------------------------

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](https://proofassistants.stackexchange.com/questions/397/are-eliminators-useful-in-practice-or-are-they-only-useful-in-the-metatheory) and in [this answer](https://proofassistants.stackexchange.com/a/327) 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.