# Exponentiation Functor is Functor

## Theorem

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

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

Let $\left({-}\right)^A: \mathbf C \to \mathbf C$ be the exponentiation functor.

Then $\left({-}\right)^A$ is a functor.

## Proof

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

Let $\epsilon_B: B^A \times A \to B$ be the evaluation morphism at $B$.

Then, since:

 $\ds \operatorname{id}_B \epsilon_B$ $=$ $\ds \epsilon_B$ $\ds$ $=$ $\ds \epsilon_B \operatorname{id}_{B^A \times A}$ $\ds$ $=$ $\ds \epsilon_B \left({\operatorname{id}_{B^A} \times \operatorname{id}_A}\right)$

it follows that $\left({\operatorname{id}_B}\right)^A = \operatorname{id}_{B^A}$.

Next, let $f: B \to C, g: C \to D$ be composable morphisms.

Then:

 $\ds g f \epsilon_B$ $=$ $\ds g \epsilon_C \left({f^A \times \operatorname{id}_A}\right)$ Definition of $f^A$ $\ds$ $=$ $\ds \epsilon_D \left({g^A \times \operatorname{id}_A}\right) \left({f^A \times \operatorname{id}_A}\right)$ Definition of $g^A$ $\ds$ $=$ $\ds \epsilon_D \left({g^A f^A \times \operatorname{id}_A}\right)$

Thus, $g^A f^A$ is the morphism satisfying the UMP for $\left({g f}\right)^A$.

That is to say:

$\left({g f}\right)^A = g^A f^A$

Hence, $\left({-}\right)^A$ is a functor.

$\blacksquare$