definition. exponential [kostecki2011introduction, 5.13] [tt-004G]

✍️source

If for \(X \in {\cal C}\), a cartesian product functor \(X \times (-)\) has a right adjoint, it is called an exponential or the exponential object, denoted \((-)^X\).

Explicitly, \(X \times (-) \dashv (-)^X\) means there is a natural isomorphism of bifunctors \(\operatorname {Hom}(X \times (-),-) \cong \operatorname {Hom}(-, (-)^X)\), i.e. for any arrow \(f: X \times Y \to Z\) there is a unique arrow \(f^b: Y \to Z^X\), which is the transpose of the adjunction, called exponential transpose.

The arrow \(\operatorname {ev} : X \times (-)^X \to (-)\) is called the evaluation arrow of the exponential, and is the counit of the adjunction.

Diagramatically, the diagram commutes.

We say that category \({\cal C}\) has exponentials if for any \(X \in {\cal C}\), there exists an exponential \((-)^X\).