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 , the inverse laws for currying and evaluation validate this conversion as well as beta reduction.
New to topics? Read the docs here!