Contravariant Yoneda lemma

I am learning category theory and trying to prove the contravariant Yoneda lemma:

Let $$\mathcal C$$ be a locally small category and $$F:\mathcal C\to\mathsf{Set}$$ be a contravariant functor. Fix an object $$c\in\mathcal C_0$$. Then the function $$\Phi:\operatorname{Nat}\left(\operatorname{Hom}_\mathcal C(-,c),F\right)\to F(c),\qquad \Phi(\alpha)=\alpha_c(\mathrm{id}_{c})$$ is a bijection.

I want to prove it using the covariant Yoneda lemma and duality, but I am a little confused. This stackexchange question partially explains the answer, but I think it is sketchy and it does not explain how the natural transformations between contravariant functors correspond to the usual natural transformations. This is exactly what I am confused by.

Can somebody give a fully rigorous proof of this fact? Thank you!

A contravariant functor $$C\to D$$ is the same thing as a covariant functor $$C^{op}\to D.$$ So the category of contravariant functors $$C\to D$$ is the same thing as the category of covariant functors $$C^{op}\to D.$$ So a natural transformation between two contravariant functors $$C\to D$$ is the same thing as a natural transformation between two covariant functors $$C^{op}\to D$$.
The covariant Yoneda lemma is $$\operatorname{Hom}_{\mathrm{Set}^C}(\operatorname{Hom}_C(c,-), F)\cong F(c)$$ for $$c\in C$$ and $$F:C\to \mathrm{Set}$$.
Substituting $$C$$ with $$C^{op}$$ and using the fact that $$\operatorname{Hom_{C^{op}}(c,-) = \operatorname{Hom}_C(-,c)}$$ gives $$\operatorname{Hom}_{\mathrm{Set}^{C^{op}}}(\operatorname{Hom}_C(-,c), F)\cong F(c)$$ for $$c\in C$$ and $$F: C^{op}\to \mathrm{Set}.$$ This is the contravariant Yoneda lemma.
• Would it be more precise to say that $\operatorname{Hom}_{\mathcal C}(-,c)$ and $\operatorname{Hom}_{\mathcal C^\mathrm{op}}(c,-)$ are naturally isomorphic functors from $\mathcal C^\mathrm{op}$ to $\mathsf{Set}$, and hence the collection of natural transformations out of them are in bijection? Commented Aug 20, 2023 at 22:45
• @Zhuo Maybe. I meant literal identity, though. The way I view it, the objects of $C^{op}$ are literally the objects of $C$ and the set of arrows $c\to d$ in $C^{op}$ is literally the set of arrows $d\to c$ in $C.$ But there may be some benefit to viewing them as corresponding but distinct. Commented Aug 20, 2023 at 23:33