Implication Details

Assumptions: cartesian closed, copowers

Conclusions: powers

Reason: The power XIX^I can be constructed as [I⊗1,X][I \otimes 1, X] because

Hom(T,[I⊗1,X])≅Hom(T×(I⊗1),X)\mathrm{Hom}(T,[I \otimes 1, X]) \cong \mathrm{Hom}(T \times (I \otimes 1),X)

≅Hom(I⊗(T×1),X)≅Hom(I⊗T,X)\cong \mathrm{Hom}(I \otimes (T \times 1),X) \cong \mathrm{Hom}(I \otimes T,X)

≅Hom(T,X)I. \cong \mathrm{Hom}(T,X)^I.

In the second isomorphism we have used that T×−T \times - preserves copowers, which is true because it is a left adjoint.