# Is eta-equality provable in Coq?

Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove

Theorem eta : forall (A : Type) (f : A -> A), (fun x => f x) = f?


Does this require functional extensionality?

Edit: I already accepted an answer, but a better (followup) question would be, if Coq supports eta-conversion, why does Eval compute in (fun x => f x). not reduce to f?

• It should be noted that even if we have reduction rules related to eta-equality, we would usually do expansion instead of contraction, because it leads to better theoretic properties.
– Trebor
Feb 10, 2022 at 7:53
• @GuyCoder it should probably be a synonym
– Couchy
Feb 10, 2022 at 21:32

Yes, this is provable—indeed, it is provable by reflexivity. This is because Coq has eta-equality of functions built into its notion of definitional equality. Definitional equality also has a congruence rule for lambdas, which does look kind of like function extensionality, but which exists at the judgmental level, and is about definitional equality rather than propositional equality. This does not allow us to prove function extensionality, because the premise in function extensionality is a propositional equality and not a definitional one. In the presence of an equality reflection rule, this would furnish a proof of function extensionality, which is why type systems with equality reflection, eta for functions, and defeq congruence for lambdas validate function extensionality.
As for your follow-up question: Coq implements η-conversion, but not η-reduction/expansion, because η really is treated at the level of the conversion test and not at that of reduction (which is a sub-routine thereof). Concretely, the conversion test works roughly as follows when comparing t and u:
1. reduce t and u to weak head normal forms (using a bunch of reduction rules including β but not η)
2. if one of the reducts is a neutral n and the other is an abstraction fun x : A => t, recursively compare n x and t (this corresponds to η-expanding the neutral followed by a congruence rule for abstraction)