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.

Thanks for the App, that’s indeed a typo.

Looking at map-id, is there a case where
\Gamma |- (s:X) -> Y \ni f == \x -> x
would hold
\Gamma |- Set \ni X == Y
wouldn’t ?

(btw, it seems you forgot to adjust the type of the result in App)