This should presumably read “from values to terms”. I suspect your target audience won’t be confused by this, but it took me a minute or two to figure it out.

To typecheck a term, it must be beta-normal. Environment-body pairs cannot be typechecked without substituting them out (hereditarily).
To match on a term, it must be beta-delta-normal and of positive type. (Positive types are Set, Prop, enumerations, datatypes. Not Pi, Sig, proofs, codatatypes.)
To update a term, we care only that it is represented in a first-order way.
To construct a term, e.g. when implementing an operator, we like some sort of lambda (Haskell or de Bruijn), not environment-body pairs.
To go from functional binding or environment-body pairs to a first-order lambda requires a name supply.
To typecheck requires a name supply and bidirectional type information.
To eta-expand requires a name supply and bidirectional type information.
To beta-normalize or beta-delta-normalize requires only a name supply.
Whatever ‘values’ operators consume must be easily embedded anywhere in whatever they produce, without a name supply.

These constraints admit a variety of solutions. Are there more constraints?

elim_Nat Z (\n r -> S n)
elim_Nat Z (\n r -> S r)

So doing either expansion is going to leave something out, and can’t work, I suppose. Perhaps there is hope for reduction, though. As I recall, the issue with eta reduction is that it breaks confluence and uniqueness of normal forms. However, if you’re already at beta-normal forms before doing any quotation, it presumably doesn’t matter whether some non-normal term has both beta and eta redices that lead to irreconcilable terms; only beta can happen at that point.

That of course says nothing about whether detecting identity eliminations is feasible.

So, yes, (inevitably, of course), some identity functions are more equal than others. The quotation rules for map (and one or two other things) exploit structure which is present by construction. We aren’t really used to this technology yet: it certainly has many more possibilities, but we haven’t yet got a feel for what we can/should do. Interesting times. (There’s a free indexed monad just around the corner.)

f == \x -> x ==> map f x == x

Some identities are more equal than others. For instance, what if:

f = \n -> elim_Nat Z (\_ -> S) n

I guess this is more eta, so does \x -> x get expanded into the version with the eliminator (sums are part of why eta expansion is preferred, as I recall). Or does one try to recognize eliminators that just rebuild the thing they’re eliminating?

We try to write presentations of rules which give rise directly to the appropriate algorithms. Each judgment form has input positions and output positions, preconditions explaining our requirements of inputs, and postconditions giving guarantees about outputs.

In the case of Γ |- T ∋ u == v, all four positions are inputs. The preconditions are Γ |- T ∋ t and Γ |- T ∋ v. That is, to ask if two values are equal at type T, you must first know that they both have that type.

How do we use rules? We work from conclusions to premises. We may presume that the conclusion preconditions hold (or we would not be interested in the problem); we may reduce the conclusion to a collection of premises only if we can establish their preconditions, left-to-right.

Hence, indeed, we have to check that X is Y before we may ask if f is id.