Extensional reflexive object
= Extensional reflexive object
{title2=$D\cong D^D$}
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.