# How can we quickly verify naturality?

The Yoneda lemma is sometimes claimed to simplify proofs. For instance, the associativity of binary products can be proved by considering $$\hom(X, (A \times B) \times C)$$, and by the bijection of sets $$(U \times V) \times W \cong U \times (V \times W)$$ we get the result.

However, this neglects the naturality of that family of bijection. Wouldn't it be just as tedious to verify naturality as doing the proof by diagram chasing? This seems to especially be the case when equalizers and exponentials etc. are involved, so the rearrangement is non-trivial. Ascending to 2-categories, this problem only gets worse.

Is there a nice trick that reduces the work, while staying completely rigorous?

• There’s no need to chase any diagrams. You just need to build up your toolbox of basic lemmas. For example, natural transformations compose to yield natural transformations. Mar 18, 2023 at 4:54
• @ZhenLin My example above doesn't seem to be decomposable. So what you are saying is "no, we can't do this quickly", right? Because these are exactly the tools you are referring that need to be built up by hand. Mar 18, 2023 at 5:41

First: $$\textrm{Hom} (X, (A \times B) \times C) \cong \textrm{Hom} (X, A \times B) \times \textrm{Hom} (X, C)$$ This is natural in $$X, A, B, C$$ and is either by definition of $$\times$$ or a basic lemma you prove soon. Note that $$\times$$ of sets may have a different definition – it doesn't matter, as long as you are consistent. Then we repeat: $$\textrm{Hom} (X, A \times B) \times \textrm{Hom} (X, C) \cong (\textrm{Hom} (X, A) \times \textrm{Hom} (X, B)) \times \textrm{Hom} (X, C)$$ This too is natural in $$X, A, B, C$$, of course. Now, $$(\textrm{Hom} (X, A) \times \textrm{Hom} (X, B)) \times \textrm{Hom} (X, C) \cong \textrm{Hom} (X, A) \times (\textrm{Hom} (X, B) \times \textrm{Hom} (X, C))$$ naturally in $$X, A, B, C$$. This is supposed to be a lemma you already know – otherwise there is indeed no point using Yoneda for this. Now we basically reverse the earlier steps: $$\textrm{Hom} (X, A) \times (\textrm{Hom} (X, B) \times \textrm{Hom} (X, C)) \cong \textrm{Hom} (X, A) \times \textrm{Hom} (X, B \times C)$$ $$\textrm{Hom} (X, A) \times \textrm{Hom} (X, B \times C) \cong \textrm{Hom} (X, A \times (B \times C))$$ Compose all of these natural bijections to obtain: $$\textrm{Hom} (X, (A \times B) \times C) \cong \textrm{Hom} (X, A \times (B \times C))$$ Then finally use the fully-faithfulness of the Yoneda embedding to deduce: $$(A \times B) \times C \cong A \times (B \times C)$$ This is natural in $$A, B, C$$, of course.
• My main concern is exactly the step in $\mathsf{Set}$. In the category $\mathsf{Set}$, writing (a) a proof of natural associativity abstractly by universal properties, and (b) using concrete elements, the length of (a) and (b) are actually similar. So the only thing Yoneda provides in this situation is the ability to reason with elements which is more intuitive, instead of really shortening the proof, right? Mar 18, 2023 at 9:41