Eta conversion ($\lambda x.Mx{\equiv }_{\eta }M(x\notin FV(M))$)

Eta conversion expresses extensionality for a lambda abstraction whose fresh argument is only passed to a function. The side condition prevents removal of a genuine dependency. In a categorical model with $D\cong D^D$, the inverse laws for currying and evaluation validate this conversion as well as beta reduction.

The least equality on lambda terms closed under lambda application and lambda abstraction and containing beta equivalence and eta conversion, with bound names identified by alpha equivalence.