Reflexive Object

A reflexive object in a Cartesian Closed Category π’ž π’ž \mathcal{C} is an object U π‘ˆ U equipped with a pair of maps 𝗅𝖺𝗆 : ( U U , U ) : 𝗅𝖺𝗆 superscript π‘ˆ π‘ˆ π‘ˆ \mathsf{lam}:{{}(U^{U},U)} and 𝖺𝗉𝗉 : ( U , U U ) : 𝖺𝗉𝗉 π‘ˆ superscript π‘ˆ π‘ˆ \mathsf{app}:{{}(U,U^{U})} such that 𝖺𝗉𝗉 ∘ 𝗅𝖺𝗆 = m a t h r m i d i f x . . β‹„ l s e i \mathsf{app}\circ\mathsf{lam}=mathrm{id}{ifx..lse\par i} , which categorifies the usual Ξ² 𝛽 \beta law.

More succinctly, a reflexive object is an object U π‘ˆ U that is a Retract of the exponential U U superscript π‘ˆ π‘ˆ U^{U} .

A reflexive object is said to be extensional if it validates the Ξ· πœ‚ \eta law, EG: U β‰… U U π‘ˆ superscript π‘ˆ π‘ˆ U\cong U^{U} .

Examples