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 \mathbf{Set}-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) \hat A of presheaves and a Yoneda vertical arrow (1-cell) y_A \colon A \to \hat A — the Yoneda embedding. We take our guidance from the category of presheaves \hat A = [A, \mathbf{Set}], where the Yoneda functor is defined as a representable functor:

y_A a = A(-, a)

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 A to \hat A.

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, C(1, f) and C(f, 1). But it’s also possible to build a functor from a profunctor.

The rough idea is that a profunctor:

H \colon A^{op} \times B \to \mathbf{Set}.

when curried, can be seen as a functor into the presheaf category:

f_H \colon B \to (A^{op} \to \mathbf{Set})
f_H b = H \langle -, b \rangle

(Koudenburg calls this functor H^{\lambda}). I’ll use the notation \hat A for the category of presheaves on A, so we can write:

f_H \colon B \to \hat A

(In what follows, I’ll sometimes omit the subscript H.)

In components, this equivalence can be written as an invertible natural transformation:

\xi_{a b} \colon H \langle a, b \rangle \to (f_H b) \, a

There is one more detail that requires special attention: f_H b is an object in the category \hat A. What does it mean to apply this object to a? We know what it means in \mathbf{Cat}, where:

\hat A = [C^{op}, \mathbf{Set}]

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:

E \colon A^{op} \times \hat A \to \mathbf{Set}

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

H \langle a, b \rangle \cong E \langle a, f_H b \rangle

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 (\hat A , E) is sometimes called the classifier for A. It lets us classify horizontal arrows H using vertical arrows f_H.

Yoneda Embedding

We can now ask the question: What is the classifying arrow for the simplest horizontal arrow: the unit arrow? In \mathbb{P}rof, the unit arrow is the hom-profunctor A(-, =). Its classifying arrow is the functor y_A \colon A \to \hat A. The 2-cell defining this classification:

evaluates to:

A(x, a) \to E \langle x, y_A a \rangle

or, expanding E:

A(x, a) \to (y_A a) x

Compare this with the definition of the Yoneda embedding:

y_A a = A(-, a)

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:

E = \hat A (y_A, 1)

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

E = y_* = \hat A (y, 1)

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

To generalize the condition that every presheaf is a colimit of representables, we want y to be dense.

A functor is dense if its left Kan extension along itself (called the density comonad) is isomorphic to identity:

\text{Lan}_{y_*} y \cong id_y

The Adjunction

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

E \langle a , \hat F \rangle \to \hat A ( y a, \hat F )

with \hat F an object (presheaf) in \hat A and E = y_*:

In \mathbb{P}rof, this is:

\hat F a \to [A, \mathbf{Set}](A(-, a), \hat F)

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:

y^* \dashv y_*

where y^* = \hat A (1, y). The adjunction can be illustrated using the following 2-cells:

with K and L arbitrary horizontal 1-cells.

The unit of this adjunction is generated by replacing K with the unit and L with y_*.

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

1 \to y_* \odot y^*

or, in expanded notation:

A(1, 1) \to \hat A (y, 1) \odot \hat A (1, y)

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 A, to the unit arrow in \hat A. In \mathbb{P}rof, this is a natural transformation from the hom-set in A to the hom-set in the presheaf category. We recognize it as the action of the Yoneda functor on hom-sets. In fact in \mathbb{P}rof it is an isomorphism:

A(a, a') \cong \hat A (y a, y a') = [A, \mathbf{Set}](A(-, a), A(-, a'))

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 y^* \dashv y_* be an isomorphism. This, together with the density of y 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 A there exist a pair (\hat A, E \colon A \to \hat A) such that for any horizontal 1-cell H \colon A \to B there exist a vertical 1-cell f_H \colon B \to \hat A and the 2-cell \xi:

In genereal, this doesn’t nail things down enough. There may be many candidates for (\hat A, E \colon A \to \hat A) and many f_H‘s for a given H.

What we want is to be able to reconstruct H from f_H. In other words we want currying to be an isomorphism, as it is in \mathbb{P}rof:

H \langle a b \rangle \cong E \langle a, f_H b \rangle

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 (L, h, k):

This might seem like a lot to process, but there is a trick to it. In \mathbb{P}rof, we can replace X and Y with the terminal one-object/one-arrow category 1. A functor from such a category selects an object in the target category. Here, we pick two functors that select a \colon A and b \colon B:

The left hand side is a mapping * \to E \langle a, f b \rangle. The right hand side is a horizontal composition of * \to H \langle a, b \rangle and H \langle a, b \rangle \to E \langle a, f b \rangle. The first one lets us fully reconstruct H.

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 (L, h, k).