%
\label{thm:yoneda-lemma}
Let $F : \mathrm{Cat}_\tau^{\mathrm{op}} \to \mathrm{Set}$
be a presheaf and $X \in \mathrm{Cat}_\tau$ an object.
There is a natural bijection:
\[
    \boxed{%
    \mathrm{Nat}\bigl(y(X),\, F\bigr)
    \;\cong\;
    F(X).}
\]
Every natural transformation
$\eta : y(X) \Rightarrow F$
is uniquely determined
by the value $\eta_X(\mathrm{id}_X) \in F(X)$.

\textbf{The Yoneda map.}
Define $\Phi : \mathrm{Nat}(y(X), F) \to F(X)$
by $\Phi(\eta) := \eta_X(\mathrm{id}_X)$.
Since $y(X)(X) = \{\mathrm{id}_X\}$ by thinness,
this is well-defined.

\textbf{The inverse.}
Given $a \in F(X)$,
define $\eta^a : y(X) \Rightarrow F$ by:
for each $Y$,
if $Y \not\leq X$ then $\eta^a_Y$ is the empty function;
if $Y \leq X$ with unique arrow $f : Y \to X$,
set $\eta^a_Y(*) := F(f)(a)$.

\textbf{Naturality.}
For $g : Y_1 \to Y_2$ with $Y_2 \leq X$,
let $f_1 : Y_1 \to X$ and $f_2 : Y_2 \to X$
be the unique arrows.
Then
$F(g)(\eta^a_{Y_2}(*))
= F(g)(F(f_2)(a))
= F(f_2 \circ g)(a)
= F(f_1)(a)
= \eta^a_{Y_1}(*)$,
using $f_2 \circ g = f_1$ by thinness.
The case $Y_2 \not\leq X$ is vacuous.

\textbf{Bijectivity.}
$\Phi(\eta^a) = F(\mathrm{id}_X)(a) = a$,
so $\Phi \circ \Psi = \mathrm{id}$.
Conversely, given $\eta$ and $Y \leq X$
with unique $f : Y \to X$,
naturality forces
$\eta_Y(*) = F(f)(\eta_X(\mathrm{id}_X))
= F(f)(\Phi(\eta))$,
so $\eta = \eta^{\Phi(\eta)}$
and $\Psi \circ \Phi = \mathrm{id}$.