GoKawiilWorking with double categories can be aptly summarized in a meme: Talk to me about sets without mentioning sets. We don’t talk about hom-sets, we talk about horizontal units. Secretly, we are visualizing horizontal arrows as profunctors, and the unit of profunctor composition is a hom-functor.
Presheaves are defined as -valued functors, so we immediately run into a problem when trying to describe them in a double category. And without presheaves, we can’t talk about the Yoneda lemma — the workhorse of category theory.
Granted, a lot of standard categorical constructions can be generalized to use profunctors in place of presheaves, with immediate generalization to double categorical settings. This can be done with (weighted) limits, Kan extensions, categories of elements (tabulations), and many others. But sometimes you just need to talk about presheaves without mentioning presheaves.
I will first sketch the constructions in category theory and, in the next installment, show you a toy implementation in Haskell.
Overview
To translate the Yoneda construction into the language of double categories, we need to define an object (a 0-cell) of presheaves and a Yoneda vertical arrow (1-cell) — the Yoneda embedding. We take our guidance from the category of presheaves , where the Yoneda functor is defined as a representable functor:
Since in this picuture the 0-cells of a double category represent categories, with no access to their objects, we have to define everything using universal constructions.
Even the simplest thing, like the action of a presheaf on an object resulting in a set, has to be defined in bulk, as a particular horizontal arrow from to .
We would also like the Yoneda embedding to be dense– a generalization of the slogan that every presheaf is a colimit of representables. We can express this in terms of left Kan extensions, which we know how to generalize to double categories.
Finally, we want the Yoneda embedding to be full and faithful, without talking about the mapping of hom-sets.
... continue reading