Yoneda Lemma: Statement and Proof

Yoneda Lemma: Let $\mathbf{C}$ be a category, $F: \mathbf{C}^{op} \rightarrow \mathbf{Set}$ a functor (contravariant from $\mathbf{C}$ to $\mathbf{Set}$), and $A \in Ob(\mathbf{C})$. Then $\theta: Nat(H^A,F) \rightarrow F(A)$ defined by $\theta :\eta \mapsto \eta_A(1_A)$ is a bijection.

Proof: (Following Bell in Toposes and Local Set Theories)
We first show $\theta$ is injective by showing that any $\eta$ is uniquely determined by its image under $\theta$. To this end, let $B \in Ob(\mathbf{C})$. Then for $\eta \in Nat(H^A,F), \eta_B:H^A(B)=\mathbf{C}(B,A)\rightarrow F(B).$ We may assume $\mathbf{C}(B,A)\neq \emptyset$ for otherwise the $\eta_B$ is the empty map with codomain $F(B)$. Let $g \in \mathbf{C}(B,A)$. Then $g^{op}:A\rightarrow B \implies $(by contravariance of $H^A$ and $F$) $ H^A:\mathbf{C}(A,A)\rightarrow \mathbf{C}(B,A), F(g):F(A)\rightarrow F(B)$.

Then by naturality, $F(g)\eta_A = \eta_BH^A(g)$. Hence, evaluating at $1_A$, we get 
\[\eta_B(H^A(g)1_A) = \eta_B(1_Ag)=\eta_B(g) = F(g)(\eta_A(1_A)).\]
In particular, $\eta_B(g) = F(g)(\eta_A(1_A)) = F(g)(\theta(\eta))$, so that $\eta$ is completely determined by its image under $\theta$. Hence $\theta$ is injective.

Now we prove $\theta$ is surjective. Let $a \in F(a)$. We know that if $a$ is the image of some $\eta$ that $\eta$ will satisfy the above formula. So we would have
$\eta_B(g) = F(g)(\eta_A(1_A)) = F(g)(a)$ if we had $\theta(\eta)=a$.

Hence we should define $\eta$ on objects $B$ and arrows $g \in \mathbf{C}(B,A)$
by $\eta_B(g) = F(g)(a)$. We show this defines a natural transformation.
Let $B_1, B_2 \in Ob(C), f^{op}:B_1 \rightarrow B_2$. Then for
$h \in \mathbf{C}(B_1, A)$,   \[\eta_{B_2}(H^A(f)(h)) = \eta_{B_2}(hf) = F(hf)(a) = F(f)(F(h)(a)),\]
where the last equality holds because $F$ is contravariant.
However, we also have \[F(f)\eta_{B_1}(h) = F(f)(F(h)(a)).\]
Therefore \[\eta_{B_2}H^A(f) = F(f)\eta_{B_1},\] which is  the naturality condition.
Hence $\eta \in Nat(H^A,F)$. But \[\theta(\eta) = \eta_A(1_A) = F(1_A)(a) = 1_{F(A)}(a) = a.\]
So $\theta$ is also surjective.  Hence $\theta$ is a bijection, completing the proof.

If we let $F = H^B$ for another $\mathbf{C}$-object $B$, we get the immediate corollary $Nat(H^A,H^B)\cong \mathbf{C}(A,B)$ for any objects $A,B \in Ob(\mathbf{C})$.