Solution (source code)

= Solution

The covariant form of the <Yoneda lemma> says that for a <locally small category> $\mathcal C$, a <functor> $F:\mathcal C\to\mathbf{Set}$ and an object $A$, there is a <bijection>, natural in $A$ and $F$,
$$
\operatorname{Nat}(\mathcal C(A,-),F)\cong F(A).
$$
Explicitly its two directions are
$$
\boxed{\alpha\longmapsto\alpha_A(1_A),\qquad x\longmapsto\alpha^x,
\quad\alpha^x_B(f)=F(f)(x).}
$$
For $u:B\to B'$, functoriality gives $F(u)\alpha^x_B(f)=F(uf)(x)=\alpha^x_{B'}(uf)$, so $\alpha^x$ is a <natural transformation>. Conversely, naturality of $\alpha$ at $f:A\to B$ gives $\alpha_B(f)=F(f)(\alpha_A(1_A))$. This proves that the displayed maps are inverses.

Naturality in $F$ follows because postcomposition by $\theta:F\Rightarrow F'$ sends $x$ to $\theta_A(x)$. For $u:A'\to A$, precomposition of transformations by $\mathcal C(u,-)$ sends $\alpha^x$ to $\alpha^{F(u)(x)}$. This also verifies naturality in the representing object.