For a long time I felt like I didn't really understand the Yoneda Lemma. I knew some things that people said about it ('we can understand objects by the maps into them' and 'the Yoneda embedding is full and faithful') but the statement 'Hom(Hom(A, -), F) = F(A)' itself was something I could only use as a symbolic manipulation without understanding.

On the other hand, I did separately know facts like 'In the category of quivers there are objects which look like • and •→•, such that the maps out of them tell you exactly the vertices and edges in your quiver' and 'In the category of simplicial sets there are objects which are just an n-simplex; maps out of them are the n-simplices of the object you are mapping into'.

Somehow I only recently realised that these examples are precisely the Yoneda Lemma. These objects are precisely presheaves of the form Hom(A, -), and the Yoneda Lemma tells you what you get when you map out of them.

In particular I think it would be useful to give the quiver example to students when they learn the Yoneda Lemma.

#CategoryTheory #Math #Maths #Mathematics #Yoneda #YonedaLemma

Anyone want to volunteer a guide for when to use #yoneda instead of #coyoneda in #haskell or #purescript ?

I'm wanting to provide an HFunctor (https://pursuit.purescript.org/packages/purescript-fix-functor/0.1.0/docs/FixFunctor#t:HFunctor) instance but the naive way to do that requires me to "invent" a Functor instance for the source type constructor -- thinking of adding a yoneda/coyoneda wrapper and I think either would work, but I'm not sure.