It took me five days really to understand the yoneda lemma, it has a lot of moving parts. So here's my own very complete and too verbose proof of the contravariant functor version. Alt text is the pdf.
0

If you have a fediverse account, you can quote this note from your own instance. Search https://hj.9fs.net/spew/p/1767968631.062950 on your instance and quote it. (Note that quoting is not supported in Mastodon.)