Definition:Exponentiation Functor

From ProofWiki
Jump to navigation Jump to search

Theorem

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

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


Then exponentiation by $A$, denoted $\paren -^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 {\paren {f \circ \epsilon} } \)      $f: B \to C$ is a morphism of $\mathbf C$

Here $\epsilon: B^A \times A \to B$ denotes the evaluation morphism, and $\widetilde {\paren {f \circ \epsilon} }: 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


Sources