**Yoneda Lemma**

**Theorem**:
Let be a locally small category.
Let denote the Yoneda embedding.

*naturally* in both and .

*Proof*:
We start by defining a bijection between the two sets.
To do this, we’ll define functions and , then show that they compose in both directions to give the identity.

Given a natural transformation , we have a component . Note that is just . In particular, . So, define .

Given an element , we need to define a natural transformation . We will let the components be defined as follows: Given an in , the functor yields a map . So, let . To be pedantic, let’s verify that is actually natural. Consider the naturality square with respect to a map in :

Evaluating at arbitrary (i.e. ), we have (recall is right composition by ):

but is a functor and thus is associative and respects composition (switching the order due to contravariance), so the top and bottom expressions are equal.

We’ve defined the two functions. Now we must show that they compose to the identity in both directions.

Take an . We must show . This amounts to showing that:

for all and . We have:

Consider the naturality square of with respect to the map :

evaluating at in the upper right yields:

which gives precisely the desired equality.

Now, given an , we must show . Indeed:

which gives the desired equality.

Now that we’ve finally established the bijection, we must show that it’s natural in both and . We start with . To be precise, we have a functor , that can realized as the compound functor . On the right we have a the functor . We must show that gives the components of a natural transformation between the two. This amounts to showing that, for a , the square:

commutes. Evaluate at an arbitrary starting from the top-right:

We show the final expressions are equal. Keeping in mind that the components of are given by left-composition by ,

And, working backwards from equalities derived earlier:

and the square commutes.

Now we show naturality in . To be precise, on the left we have the functor , which is, essentially, . On the right we have the evaluation functor . To be exceedingly clear, we clarify precisely how this is functorial by describing the behavior on maps: for a natural transformation , the functor sends to its component . We must again show that gives the components of a natural transformation between the two. That is, for arbitrary , the square:

must commute. Evaluating at an arbitrary in the top-left, we have:

but these are equal because of the definition of composition of natural transformations: . So the square commutes.

Finally, we’ve exhibited a family of isomorphisms that are *natural* in both and , completing the proof.