From Problem 13 in Chapter 6 of Awodey's book Category Theory, I am asked to show that in a cartesian closed category with coproducts, the products necessarily distribute over the coproducts.
$$
(A\times C)+(B\times C)\cong (A+B)\times C
$$
Let $\iota_1:A\to A+B$ and $\iota_2:B\to A+B$ be the inclusion maps. Let $\pi_1^A:A\times C\to A$ and $\pi_2^A:A\times C\to C$ denote the projections, and similarly define $\pi_k^B$ on the object $B\times C$ for $k=1,2.$
It seems to me that there are two natural maps $(A\times C)+(B\times C)\to(A+B)\times C,$ namely the maps $[\iota_1\times 1_C,\iota_2\times 1_C]$ and $\left((\iota_1\circ \pi_1^A)+(\iota_2\circ\pi_1^B), [\pi_2^A,\pi_2^B]\right).$ These really seem like they should be the same map, although I don't know how to prove it. Additionally, these seem like they should be isomorphisms, but I cannot find explicit inverses.
I would like to say that I am aware that this can be proven using the Yoneda lemma, but I will not have access to that until Chapter 8. I need to find a way around using that.
Best Answer
Since we're in a Cartesian closed category, denoting the internal hom as $[-,-]$, for any object $X$, we have $$\hom((A+B)\times C, \, X) \cong\hom(A+B,\, [C,X]) \cong \hom(A, [C,X])\times\hom(B, [C,X]) \cong\\ \cong\hom(A\times C,\, X) \times \hom(B\times C, \, X) \cong\hom((A\times C)+(B\times C), \, X) $$ Now, yes, you either use Yoneda lemma to conclude the required isomorphism, or you can apply the above isomorphism directly with $X=(A+B)\times C$ and $X=(A\times C) +(B\times C)$, picking the correspondent of the respective identity morphisms, and apply naturality.