Solution (source code)

= Solution

For a <locally small category> $\mathcal C$, an object $C$, and a <categorical presheaf> $X:\mathcal C^{\mathrm{op}}\to\mathbf{Set}$, the <Yoneda lemma> gives the <natural bijection>
$$
\boxed{\Phi_{C,X}:\operatorname{Nat}(\mathcal C(-,C),X)\cong X(C).}
$$
Its two maps are explicitly
$$
\Phi_{C,X}(\alpha)=\alpha_C(1_C),\qquad
\Psi_{C,X}(x)_A(f)=X(f)(x)\quad(f:A\to C).
$$
For $u:A'\to A$, the equation $X(u)X(f)(x)=X(fu)(x)$ proves <naturality> of $\Psi(x)$. Evaluating it at the <identity morphism> gives $\Phi\Psi(x)=x$. Conversely, <naturality> of $\alpha$ at $f:A\to C$ gives
$$
\alpha_A(f)=X(f)(\alpha_C(1_C)),
$$
so $\Psi\Phi(\alpha)=\alpha$. \b[Evaluation at the identity and transport of an element along a morphism are mutually inverse.]

The <bijection> is natural in both variables: a <natural transformation> $\theta:X\Rightarrow Y$ sends $\Phi(\alpha)$ to $\theta_C(\Phi(\alpha))$, matching $\Phi(\theta\alpha)$; and $g:C\to C'$ gives
$$
\Phi_{C,X}(\alpha\circ\mathcal C(-,g))
=X(g)(\Phi_{C',X}(\alpha))
\quad\bigl(\alpha:\mathcal C(-,C')\Rightarrow X\bigr).
$$
For completeness, the covariant <Yoneda lemma> for $Y:\mathcal C\to\mathbf{Set}$ is $\operatorname{Nat}(\mathcal C(C,-),Y)\cong Y(C)$, with $\alpha\mapsto\alpha_C(1_C)$ and inverse $y\mapsto(f:C\to A\mapsto Y(f)(y))$.