Eta-equivalence

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.

$A ::= a \mid A_1 \rightarrow A_2$

$e ::= x \mid \lambda x{:}A.\, e \mid e_1\ e_2$

Eta-equivalence for terms $\texttt{}e : A \rightarrow B$ is the least congruence relation $\texttt{}e_1 =_\eta e_2$ closed under the $\texttt{}\eta$ axiom:

${(x \not\in \mathit{FV}(e)) \over \lambda x{:}A.\, e\ x =_\eta e} \eta$

In logics and typed calculi, eta-equivalence is usually oriented to the left yielding a notion of eta-expansion. For example:

$e : A \rightarrow B \Longrightarrow_\eta \lambda x{:}A.\, e\ x$

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.