From The Twelf Project
Eta-equivalence (η-equivalence) is a notion of proof equivalence in natural deduction logics with introduction and elimination forms. Roughly, it says that any proof of a proposition is equivalent to one which introduces the proposition's principal connective. It is a form of extensional equivalence.
Consider the simply-typed lambda-calculus with arrow types.
Eta-equivalence for terms is the least congruence relation closed under the axiom:
In logics and typed calculi, eta-equivalence is usually oriented to the left yielding a notion of eta-expansion. For example:
Eta-expansion transforms an arbitrary proof of a proposition into a proof that introduces the proposition's principal connective. A term with no sub-terms that can be eta-expanded without introducing beta-redexes is said to be eta-long. Being eta-long is one aspect of being canonical.