Theorem: Let be a locally small category and suppose . If then . In other words, the Yoneda embedding is injective on isomorphism classes of objects.
Proof: means we have a natural isomorphism . It has components , which are also isomorphisms (in particular, the hom-sets are in bijection). Consider and denote . We claim that this is the isomorphism desired. Indeed, first look at the naturality square of with respect to the arrow :
(the horizontal arrows in the opposite direction because is contravariant). Keep in mind the vertical arrows are bijections. The horizontal maps on both top and bottom are given by definition as right-composition by , i.e. . Since the vertical maps are bijections, we have an mapping onto via . Evaluating the diagram at then gives:
Then commutativity says . But was defined to be the image of under the bijection , so .
Let’s look now at the naturality diagram with respect to this map :
where we’ve swapped the vertical arrows with their inverses, for convenience. If we evaluate this diagram at :
we get . But was defined to be the preimage of under , so we have .
Then, (or ) is the desired isomorphism between and .