Using Yoneda to establish natural isomorphisms

category-theorynatural-transformationsyoneda-lemma

I know the Yoneda embedding can be used to easily establish isomorphisms between objects in categories. For example, in a locally small cartesian closed category $\mathbf{C}$ with coproducts, the "distributivity" isomorphism
$$(A\times B)+(A\times C)\cong A\times(B+C)\tag{1}$$
follows from the natural isomorphism
$$y((A\times B)+(A\times C))\cong y(A\times(B+C))\tag{2}$$
where $y:\mathbf{C}^{\mathrm{op}}\to\mathbf{Sets}^{\mathbf{C}}$ is the (contravariant) Yoneda embedding. The natural isomorphism (2) follows fairly easily from the universal properties of the relevant objects in $\mathbf{C}$.

Is it also possible to (easily) establish the naturality of the isomorphism (1) using the Yoneda embedding? For example, to show naturality in $A$? My initial thoughts are:

  • If I can show, for $f:A\to A'$ in $\mathbf{C}$, commutativity of the embedding of the relevant naturality square, then naturality follows since the embedding is faithful. But this approach doesn't seem to make my life any easier. (Maybe for some problems it does?)
  • If $\mathbf{C}$ is small, then $\mathbf{C}^{\mathbf{C}}$ is locally small, so I could consider the embedding $\mathbf{y}:(\mathbf{C}^{\mathbf{C}})^{\mathrm{op}}\to\mathbf{Sets}^{\mathbf{C}^{\mathbf{C}}}$ and try to establish a natural isomorphism $\mathbf{y}(F)\cong\mathbf{y}(G)$, where $F,G:\mathbf{C}\to\mathbf{C}$ are the functors (of $A$) on the left and right sides of (1). But this seems even more insane.
  • If there is a "higher level" naturality relationship between the natural isomorphisms in (2), perhaps I could use that to easily establish naturality of (1). But I'm not sure if there is one, since I haven't studied much higher category theory yet.

It's also possible I'm missing something more obvious.

I ask because in Awodey's book Category Theory, 2nd ed., in Proposition 8.6 on p. 193, Awodey purports to establish the "canonical" isomorphism (1) using Yoneda. However, if "canonical" means natural, I don't see how that follows from his proof; and if "canonical" means something else, I don't know what he's talking about.

Best Answer

After working more problems, I see that the approach indicated in my first bullet point above can make my life easier, because it ultimately reduces the problem to showing commutativity of squares like $\require{AMScd}$ \begin{CD} \mathrm{Hom}(FA,X) @<{\cong}<< \mathrm{Hom}(GA,X)\\ @A (Ff)^* AA @AA (Gf)^* A\\ \mathrm{Hom}(FA',X) @<<{\cong}< \mathrm{Hom}(GA',X) \end{CD} and that is often not hard. Then the result follows by faithfulness of the Yoneda embedding (or by taking $X=GA'$ and chasing $1_{GA'}$ around the diagram).