CatDat

Implication Details

Assumptions: cartesian closed, copowers

Conclusions: powers

Proof: The power $X^I$ can be constructed as $[I \otimes 1, X]$ because $$\begin{align*} \Hom(T,[I \otimes 1, X]) & \cong \Hom(T \times (I \otimes 1),X) \\ & \cong \Hom(I \otimes (T \times 1),X) \\ & \cong \Hom(I \otimes T,X) \\ & \cong \Hom(T,X)^I. \end{align*}$$ In the second isomorphism we have used that $T \times -$ preserves copowers, which is true because it is a left adjoint.