 Extensional reflexive object

An object isomorphic to its own exponential supplies mutually inverse folding and unfolding maps. Evaluation defines application, and folding after currying defines abstraction. The exponential universal property gives the beta rule, while the full isomorphism gives eta conversion. A mere retraction of the function object generally suffices for beta but not automatically eta.