Structure

Implication details

Claim: If a category is cartesian closed and has copowers, then it has powers.

Proof: 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)≅Hom⁡(I⊗(T×1),X)≅Hom⁡(I⊗T,X)≅Hom⁡(T,X)I.\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×−T \times - preserves copowers, which is true because it is a left adjoint.

This implication has a dual.

Show 17 categories using this implication