Exponentiation Functor is 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$.

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

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


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.


\(\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.