Definition:Exponentiation Functor

From ProofWiki
Jump to navigation Jump to search


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