Double Category | Bartosz Milewski's Programming Cafe

September 13, 2026

Yoneda Lemma in Double Categories

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)$ .

June 13, 2026

Kan Extensions in Double Categories

Posted by Bartosz Milewski under Category Theory, Double category, Haskell, Kan extensions, Profunctor Equipment | Tags: Category Theory, Double Category, Profunctors |
Leave a Comment

Previously: Kan extensions in Haskell.

In a double category that is also a proarrow equipment, we have the ability to bend arrows. In particular, in the definition of the counit of the right Kan extension:

we can bend the vertical $j$ arrow, replacing it with its horizontal conjoint $B(1, j)$ . In a profunctor equipment, this is just a representable profunctor $\langle b, a\rangle \mapsto B(b, j a)$ .

A natural generalization is to replace this representable with a general profunctor. This way we get a definition of a right Kan extension along a profunctor $J$ .

In a more general setting of a double category, the counit of the right Kan extension is a 2-cell:

The universal condition can be similarly generalized by bending the $j$ arrows.

However, the universal condition for pointwise right Kan extensions is stronger. It involves an additional horizontal 1-cell $H$ . It states that any 2-cell $\phi$ of the shape below can be uniquely factorized through the counit $\epsilon$ :

Right Kan extensions in Haskell

In Haskell, the right Kan extension of a functor d along a profunctor j can be written as a data type:

newtype Ran j d a = Ran (forall x . j a x -> d x)

This is a direct translation of the categorical formula that uses an end:

$(\text{Ran}_J d) \, a = \int_x \text{Set}(J a x, d \, x)$

Compare this with the earlier implementation of the Kan extension, in which j was a functor:

newtype Ran j d a = Ran (forall x . (a -> j x) -> d x)

The counit is a 2-cell from j to the identity profunctor (->):

			
epsilon :: (Profunctor j, Functor d) => 
  Cell (Ran j d) d j (->)
epsilon jab (Ran ran) = ran jab

The 2-cell Phi goes from the profunctor composition of j and h to the identity profunctor:

type Phi s d j h  = Cell s d (Procompose j h) (->)

The factorization cell Phi' goes from h to identity:

type Phi' s d j h = Cell s (Ran j d) h (->)

For any Phi, we can find the corresponding Phi':

			
rightAdj :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
        Phi s d j h -> Phi' s d j h
rightAdj phi hac sa = Ran (\ jcb -> phi (Procompose jcb hac) sa)

This function replaces the right adjoint used in the traditional definition of a Kan extension.

The result satisfies the factorization property:

			
factor :: (Profunctor j, Profunctor h, Functor d, Functor s) => 
  Phi s d j h -> Phi s d j h
factor phi = funComp . vcomp (rightAdj phi) epsilon

Here vcomp is the vertical composition of 2-cells:

			
vcomp :: (Functor f, Functor g, Functor h
         , Profunctor p, Profunctor q, Profunctor r, Profunctor s) =>
  Cell f g p r -> Cell g h q s 
  -> Cell f h (Procompose q p) (Procompose s r)
vcomp fg_pr gh_qs (Procompose qxc pax) 
    = Procompose (gh_qs qxc) (fg_pr pax)

		

and funComp is hom-functor composition:

			
funComp :: Procompose (->) (->) a b -> (a -> b)
funComp (Procompose f g) = f . g

The computational meaning of the universal construction is that, in order to define a 2-cell (natural transformation) from some functor s to Ran j d along a profunctor h, it’s enough to provide a 2-cell from s to d along a composite Procompose j h.

Left Kan extensions

We can apply similar generalization to left Kan extensions. This time we start with the unit given by the 2-cell:

The universal condition that defines the pointwise left Kan extension of a vertical 1-cell $d$ along a horizontal 1-cell $J$ is given by the following unique factorization:

Left Kan extensions in Haskell

In Haskell, we define the left Kan extension along a profunctor as an existential data type:

			
data Lan j d a where
    Lan :: j x a -> d x -> Lan j d a

This is a direct translation of the coend formula:

$(\text{Lan}_J d)\, a = \int^x ( J x a \times d \,x)$

The unit is a 2-cell:

			
eta :: (Profunctor j, Functor d) => Cell d (Lan j d) j (->)
eta jab da = Lan jab da

The universal condition states that, for any 2-cell:

type Phi s d j h  = Cell d s (Procompose h j) (->)

there is a unique 2-cell:

type Phi' s d j h = Cell (Lan j d) s h (->)

given by the mapping:

			
leftAdj :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
        Phi s d j h -> Phi' s d j h
leftAdj phi hac (Lan jxa dx) = phi (Procompose hac jxa) dx

that uniquely factorizes through the unit eta:

			
factor :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
    Phi s d j h -> Phi s d j h
factor phi = funComp . vcomp eta (leftAdj phi)

Again, computationally, this defines a mapping-out property of the left Kan extension.

Complete Haskell code is available here: left Kan extensions, right Kan extensions.

April 24, 2026

Profunctor Equipment

Posted by Bartosz Milewski under Category Theory | Tags: Category Theory, Companion, Conjoint, Double Category, Proarrow Equipment, Profunctors, String Diagrams |
1 Comment

The fundamental premise of category theory is that it’s possible to fully capture the nature of objects by describing their interactions with other objects of the same type. Those interactions are encoded using morphisms: arrows between objects.

What about categories themselves? We define a category by describing its internals: objects and arrows. But true to the categorical credo, we should be able to capture the essence of a category by describing its interactions with other categories. (Small) categories are objects in the category of categories $Cat$ , with functors as morphisms.

In fact $Cat$ has even more structure: functors between any two categories form a functor category, with natural transformations as morphisms. This makes $Cat$ a 2-category, with categories as 0-cells, functors as 1-cells, and natural transformations as 2-cells.

With this much structure, we can define a lot of categorical constructions. In particular, we can define adjunctions as pairs of functors equipped with the unit and counit natural transformations. We can also define monads as endofunctors equipped with the unit and multiplication natural transformations, and so on.

However, there are some categorical constructions that force us to look at the internals of categories. In particular, anything that involves representable functors cannot be defined without talking about hom-sets, which are internal to categories. In particular there are things like (weighted) limits or pointwise Kan extensions that rely on representability.

We somehow need to incorporate the information about hom-sets into the fabric of of the 2-category $Cat$ . At the minimum, we need to identify the hom-functors:

$C(-, =) \colon C^{op} \times C \to Set$

Such functors of mixed variance are called profunctors and, in general, they can go between different categories, as in $P \colon C^{op} \times D \to Set$ . In fact, profunctors can be considered arrows in the category $Prof$ . Not only that, $Prof$ is itself a bicategory, whose 0-cells are (small) categories, 1-cells are profunctors, and 2-cells are natural transformations between profunctors. Composition of profunctors is defined using the coend formula:

$(Q \odot P)\langle a, b \rangle = \int^{x \colon X} Q \langle a, x \rangle \times P \langle x, b \rangle$

To be consistent with the Haskell implementation, I picked the arrow order, so you can read it $Q$ then $P$ .

What is important is that the hom-functor $C(-, =)$ is the identity profunctor with respect to this composition. It means that we have a way of talking about hom-sets and representables without peeking inside individual categories.

The usual categorical laws, associativity and identity, are only satisfied up to isomorphism (that is up to invertible 2-cells), hence $Prof$ is called a bicategory and not a 2-category, whose laws are satisfied on the nose.

These two categories, the 2-category $Cat$ and the bicategory $Prof$ can be combined into a single double category, which we’ll call $\mathbb{P}rof$ . The 0-cells are the usual categories; but now we have two kinds of arrows: the vertical ones are functors, and the horizontal ones are profunctors. What glues them together are the 2-cells.

Here’s a 2-cell that combines two (vertical) functors $f \colon A \to B$ and $g \colon C \to D$ with two (horizontal) profunctors $H \colon A \to C$ and $J \colon B \to D$ .

In our double category $\mathbb{P}rof$ , this 2-cell is implemented as a natural transformation, whose component at the pair of objects $\langle a, c \rangle$ is a function:

$\alpha_{\langle a, c \rangle} \colon H \langle a, c \rangle \to J \langle f a, g c \rangle$

It’s a member of the set of natural transformations, which can be written as an end:

$\int_{a c} Set(H \langle a, c \rangle, J \langle f a, g c \rangle)$

The profunctor $J \langle f a, g c \rangle$ is sometimes called the restriction of $J$ along $f$ and $g$ .

In an abstract double category, a 2-cell is just something that says that the particular four arrows in this configuration are related.

The same diagram can be transformed into a string diagram. Here, the 0-cells are the four areas, 1-cells form boundaries between those areas, and a 2-cell is a node connecting the four subdivisions:

We encode identity 1-cells in string diagrams by simply omitting the corresponding lines/arrows.

2-cells can be composed both horizontally and vertically by gluing them along identical edges.

In $\mathbb{P}rof$ , horizontal composition of 2-cells corresponds to the (vertical) composition of natural transformations between profunctors (we’ll write this composition as a juxtaposition, as in $\alpha \beta$ , in diagram order).

The identity 2-cell at a profunctor $P$ is just an identity natural transformation:

Vertical gluing of string diagrams results is a natural transformation between composite profunctors. For instance this diagram:

is a composition of two natural transformation:

$\alpha_{\langle a, c \rangle} \colon P \langle a, c \rangle \to R \langle f a, g c \rangle$
$\beta_{\langle c, e \rangle} \colon Q \langle c, e \rangle \to S \langle g c, h e \rangle$

whose component is a function:

$(\alpha \odot \beta)_{\langle a, e \rangle} \colon \int^c P\langle a, c \rangle \times Q \langle c, e \rangle \to \int^{c'} R \langle f a, g c' \rangle \times S \langle g c', h e \rangle$

By co-continuity of the coend, this is isomorphic to:

$\int_c \big(P\langle a, c \rangle \times Q \langle c, e \rangle \to \int^{c'} R \langle f a, g c' \rangle \times S \langle g c', h e \rangle \big)$

and is implemented by composing the product $\alpha_{\langle a, c \rangle} \times \beta_{\langle c, e \rangle}$ with the appropriate injection into the coend.

The unit of vertical composition at a functor $f$ in $\mathbb{P}rof$ is a 2-cell:

which is a natural transformation $A(a, a') \to B(f a, f a')$ implementing the functoriality of $f$ .

Companion and Conjoint

Given a functor $f \colon A \to B$ we can construct two representable profunctors, the companion and the conjoint.

The companion is denoted by $B(f, 1)$ or $f_*$ . In $\mathbb{P}rof$ , it is the profunctor generated by the following hom-functor:

$\langle a, b \rangle \mapsto B (f a, b )$

A conjoint, which is denoted by $B(1, f)$ or $f^*$ , is defined in $\mathbb{P}rof$ as:

$\langle b, a \rangle \mapsto B (b, f a)$

Notice that these two horizontal arrows go in opposite directions. The companion goes from $A$ to $B$ (the same as $f$ ), and the conjoint goes from $B$ to $A$ . Later we’ll see that they form an adjunction.

In these definitions we have used the hom-sets explicitly, something we were trying to avoid. We should therefore try to define the companions and the conjoints abstractly by listing their properties.

Companion

In a string diagram, the companion of a vertical arrow $f \colon A \to B$ is represented by a left-pointing horizontal arrow:

It is equipped with two 2-cells called the unit and the counit (the subscript $p$ stands for comPanion):

Indeed, using the rules for reading string diagrams in $\mathbb{P}rof$ , the unit corresponds to a natural transformation:

$\eta_{\langle a, a' \rangle} \colon A (a, a') \to B (f a, f a' )$

which just expresses the functoriality of $f$ . The (invisible) horizontal line on the left stands for the identity profunctor $A(a, a')$ .

The counit in $\mathbb{P}rof$ :

$\epsilon_{\langle a, b \rangle} \colon B (f a, b) \to B (f a, b)$

is trivially instantiated by the identity natural transformation.

There are two ways we can compose these two 2-cells. Both of them should result in some kind of identities. For instance, this is the horizontal composition:

$\eta \epsilon = id_f$

where $id_f$ is the identity at $f$ which, in $\mathbb{P}rof$ is a functorial action of $f$ on the hom-set.

Similarly, vertical composition gives us:

$\epsilon \odot \eta = id_{B(f, 1)}$

Conjoint

The conjoint of $f \colon A \to B$ is represented by the right-pointing horizontal arrow:

In $\mathbb{P}rof$ , the conjoint is the representable profunctor: $\langle b, b' \rangle \mapsto B(b, f b')$

The conjoint is related to the original functor by its unit and counit 2-cells:

(here, the subscript $j$ stands for conJoint). Their two compositions produce identity 2-cells:

$\eta \epsilon = id_f$
$\eta \odot \epsilon = id_{B(1, f)}$

Adjunction

We can also compose units with units and counits with counits by connecting the functor arrows:

These diagrams can be interpreted as the unit and counit of the adjunction $B(1, f) \dashv B(f, 1)$ :

$\eta \colon id_A \to B(f, 1) \odot B(1, f)$

$\epsilon \colon B(1, f) \odot B(f, 1) \to id_B$

In $Prof$ , the profunctor composition is given by the coend, so we get, for the unit:

$\eta \colon A(a, a') \to \int^b B(f a, b) \times B(b, f a')$

We use the Yoneda reduction to eliminate the coend:

$\int^b B(f a, b) \times B(b, f a') \cong B(f a, f a')$

The unit is then instantiated by the functoriality of $f$ .

The counit is:

$\int^a B(b, f a) \times B(fa, b') \to B(b, b')$

By co-continuity of the coend, this is isomorphic to:

$\int_a \big(B(b, f a) \times B(fa, b') \to B(b, b')\big)$

which is inhabited by the composition of hom-sets.

The Big Picture

We’ve seen how to combine the 2-category $Cat$ with the bicategory $Prof$ into one double category $\mathbb{P}rof$ . In this double category every vertical arrow has a horizontal companion and every companion has a conjoint. A double category with this kind of structure is called a proarrow equipment. It has just enough structure to define abstractly such categorical constructions as weighted limits or pointwise Kan extensions. We can then apply those constructions to other double categories, without having to repeat ourselves.

One immediate application is to enriched categories and enriched profunctors, which form a proarrow equipment $\mathbb{V}\text{-Cat}$ . Or we can consider a simpler case of the double category of sets and relations. We can also add more structure to the categories in question, for instance by considering monoidal categories; or even go meta, and study the double category of (weak) double categories $\mathbb{D}bl$ .

Bartosz Milewski's Programming Cafe