Yoneda Lemma in Double Categories |   Bartosz Milewski's Programming Cafe

Home
About

  Bartosz Milewski's Programming Cafe
Category Theory, Haskell, Concurrency, C++

September 13, 2026

Yoneda Lemma in Double Categories

Posted by Bartosz Milewski under Category Theory, Profunctor Equipment | Tags: Category Theory, Double Category, Proarrow Equipment, Profunctors, Yoneda Structure |
[2] Comments 

Working 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.
Most of this stuff can be expressed using 2-cells, which we can visualize using string diagrams. The problem is that a 2-cell translates into a one-way mapping, from left to right. What we often need is isomorphisms, which require some 2-cells to be invertible.
Classifying Arrows
It’s easy to turn a functor into a profunctor. In fact there are two canonical ways of defining representable profunctors. In a proarrow equipment they correspond to the companion and the conjoint, and . But it’s also possible to build a functor from a profunctor.
The rough idea is that a profunctor:
.
when curried, can be seen as a functor into the presheaf category:

(Koudenburg calls this functor ). I’ll use the notation for the category of presheaves on , so we can write:

(In what follows, I’ll sometimes omit the subscript .)
In components, this equivalence can be written as an invertible natural transformation:

There is one more detail that requires special attention: is an object in the category . What does it mean to apply this object to ? We know what it means in , where:

is a functor category. We don’t think twice about applying functors to objects. But what it really means is that we are using the counit of the currying adjunction, the evaluation (pro-)functor:

The currying of the profunctor can thus be written, in full generality, as:

One direction, left to right, of this identity can be illustrated as a double-categorical 2-cell:

We get the other direction by requiring this square to be cartesian (see Appendix 1).
The pair is sometimes called the classifier for . It lets us classify horizontal arrows using vertical arrows .
Yoneda Embedding
We can now ask the question: What is the classifying arrow for the simplest horizontal arrow: the unit arrow? In , the unit arrow is the hom-profunctor . Its classifying arrow is the functor . The 2-cell defining this classification:

evaluates to:

or, expanding :

Compare this with the definition of the Yoneda embedding:

You may also recognize this 2-cell as a definition of the unit of a companion. Thus, in a proarrow equipment, the evaluation profunctor can be seen as a companion to the Yoneda functor:

The terse notation for the companion of a functor is , so we ofter write (omitting the subscript ):

With this definition of , and with the bending of the arrow, we can redraw the original diagram defining the currying of :

To generalize the condition that every presheaf is a colimit of representables, we want to be dense.
A functor is dense if its left Kan extension along itself (called the density comonad) is isomorphic to identity:

The Adjunction
In a proarrow equipment, the counit of the companion is a 2-cell:

with an object (presheaf) in and :

In , this is:

Observe that this is half of the Yoneda lemma. In general, the other half– right to left– doesn’t automatically hold in an equipment.
In an equipment, the conjoint is the left adjoint of the companion. In the case of the Yoneda arrow, the adjunction reads:

where . The adjunction can be illustrated using the following 2-cells:

with and arbitrary horizontal 1-cells.
The unit of this adjunction is generated by replacing with the unit and with .

Thus the unit provides us with the one-way mapping:

or, in expanded notation:

In a proarrow equipment, we can straighten the two arrows to get the 2-cell:

This is interpreted as a mapping from the unit arrow (horizontal-, thus elided) in , to the unit arrow in . In , this is a natural transformation from the hom-set in to the hom-set in the presheaf category. We recognize it as the action of the Yoneda functor on hom-sets. In fact in it is an isomorphism:

which is the usual proof that the Yoneda embedding is fully faithful.
This is not an isomorphism in an arbitrary equipment, though.
We will therefore impose the condition that the unit of the adjunction be an isomorphism. This, together with the density of will single out the equipments with the Yoneda structure. Such equipments have the presheaf objects and well-behaved Yoneda embeddings.
I’m grateful to John Baez for constructive criticism.
Appendix 1
The currying condition tells us that for any 0-cell there exist a pair such that for any horizontal 1-cell there exist a vertical 1-cell and the 2-cell :

In genereal, this doesn’t nail things down enough. There may be many candidates for and many ‘s for a given .
What we want is to be able to reconstruct from . In other words we want currying to be an isomorphism, as it is in :

This can be accomplished by requiring that the above 2-cell be a cartesian square. A cartesian square is defined by a universal condition with a trio of probes :

This might seem like a lot to process, but there is a trick to it. In , we can replace and with the terminal one-object/one-arrow category . A functor from such a category selects an object in the target category. Here, we pick two functors that select and :

The left hand side is a mapping . The right hand side is a horizontal composition of and . The first one lets us fully reconstruct .
In a general double category we might not have a terminal 0-cell to select global elements, so we use the next best thing: generalized elements given by the trio .
Share this:
Share on Reddit (Opens in new window)
Reddit
More
Share on X (Opens in new window)
X

Share on LinkedIn (Opens in new window)
LinkedIn

Share on Facebook (Opens in new window)
Facebook

Email a link to a friend (Opens in new window)
Email
Like this:Like Loading…

Related

2 Responses to “Yoneda Lemma in Double Categories”

naso Says:

September 13, 2026 at 11:19 am
“the slogan that every presheaf is a coproduct of representables”
did you mean colimit?

Loading...

0x1 Says:

September 13, 2026 at 12:21 pm
aplty -> aptly ? 🙂

Loading...

Leave a ReplyCancel reply

Archived Entry

Post Date :
September 13, 2026 at 5:23 am
Category :
Category Theory, Profunctor Equipment
Tags: Category Theory, Double Category, Proarrow Equipment, Profunctors, Yoneda Structure Do More :
You can leave a response, or trackback from your own site.

Powered by WordPress.com.

Discover more from   Bartosz Milewski's Programming Cafe
Subscribe now to keep reading and get access to the full archive.

Type your email…

Subscribe

Continue reading

Loading Comments...

Write a Comment...

Email (Required)

Name (Required)

Website

%d

The text explores the application and generalization of the Yoneda lemma within the framework of double categories, focusing on the use of profunctors as a generalization of presheaves. The author notes that working with double categories often necessitates viewing horizontal arrows as profunctors, where the unit of profunctor composition relates to a hom-functor. While standard categorical constructions can be generalized using profunctors, applying the Yoneda lemma requires specific constructions within the double categorical setting.

Translating the Yoneda construction into double categories requires defining an object (0-cell) of presheaves and a Yoneda vertical arrow (1-cell), leveraging universal constructions since direct access to objects is limited. The fundamental challenge is defining the action of a presheaf on an object as a horizontal arrow. The goal is to ensure the Yoneda embedding is dense, generalizing the notion that every presheaf is a colimit of representables, which is captured by left Kan extensions generalized to double categories. Furthermore, the embedding must be full and faithful, which relates to the invertibility of certain 2-cells.

The text details how to relate a profunctor to a functor into the presheaf category through currying and evaluation. This involves defining a classifying arrow that relates horizontal arrows to vertical arrows via 2-cells. The construction of this classification hinges on ensuring that the currying condition behaves as an isomorphism. This is achieved by imposing a cartesian square condition on the defining 2-cell, which allows for the reconstruction of the object from the horizontal data, extending the concept of generalized elements when a terminal object is unavailable.

The Yoneda embedding is further connected to the adjoint relationship between the companion functor and the Yoneda functor. The counit of the companion is a 2-cell, and the relationship between the conjoint and the companion reveals an adjunction. This adjunction, when applied to the Yoneda arrow, yields a unit which, if made an isomorphism, enforces the Yoneda lemma. The unit of this adjunction provides a one-way mapping that corresponds to the action of the Yoneda functor on hom-sets, confirming that the Yoneda embedding is fully faithful under this condition. The text concludes by emphasizing that imposing the condition that the unit of the adjunction is an isomorphism, along with the density condition, selects those double categories that possess the desired Yoneda structure.