Definition:Exponentiation Functor

Theorem

Let $\mathbf C$ be a Cartesian closed metacategory.

Let $A$ be an object of $\mathbf C$.

Then exponentiation by $A$, denoted $\left({-}\right)^A: \mathbf C \to \mathbf C$, is the functor defined by:

			Object functor:		\(\ds C^A := C^A \)				$C^A$ is the exponential of $C$ by $A$
			Morphism functor:		\(\ds f^A := \widetilde{\left({f \circ \epsilon}\right)} \)				$f: B \to C$ is a morphism of $\mathbf C$

Here $\epsilon: B^A \times A \to B$ denotes the evaluation morphism, and $\widetilde{\left({f \circ \epsilon}\right)}: B^A \to C^A$ is the exponential transpose of $f \circ \epsilon$.

That it is in fact a functor is shown on Exponentiation Functor is Functor.

Also see

• Exponential (Category Theory)