Profunctor Equipment

Archived Posts from this Category

September 21, 2026

Tannakian Reconstruction in a Yoneda Equipment

The reason I bored you with the Yoneda equipment was to eventually double back to Tannakian reconstruction.

In a nutshell, Tannakian reconstruction lets us reconstruct the hom-set from a set of natural transformations between fiber functors:

$\int_{\hat F \colon \hat A} \mathbf{Set}( \hat F a, \hat F b) \cong A(b, a)$

Here, the end goes over the presheaf category.

We have previously learned that we can define a presheaf object in a double category, together with the evaluation functor $E$ that works exactly like the fiber functor:

$E \langle a, \hat F \rangle = \hat F a$

In an equipment, we can define it as a companion to the Yoneda functor:

$E = y_*$

Furthermore, in a Yoneda equipment, as a generalization of full-faithfullness, we postulate that the unit of the adjunction:

$y^* \dashv y_*$

is an isomorhpism:

$1 \cong y_* \odot y^*$

The only missing piece of the puzzle is to realize that the end in the Tannakian formula is the right Kan lift.

Right Kan Lift

The right Kan Lift is defined as the right adjoint to postcomposition. This definition is easy to interpret when only functors are involved, because postcomposition is well defined: Postcomposing with $f$ is a mapping:

$g \mapsto f \circ g$

so the right lift is defined as:

$(f \circ -) \dashv \text{Rift}_f$

The order of composition of profunctors is more convention-dependent, and the convention I used was for diagram-order composition, which happens to be the opposite of functor composition.

Thus, in $\mathbb{P}rof$ , we’ll expand the adjunction to the following isomorphism of natural transformations between profunctors:

$(S \odot P \Rightarrow Q) \cong (S \Rightarrow \text{Rift}_P Q)$

In components, the left hand side is a double end:

$\int_{a, c} (S \odot P) \langle a, c \rangle \to Q\langle a, c \rangle$

Expanding the profunctor composition, we get:

$\int_{a, c} \big( \int^b S \langle a, b \rangle \times P \langle b, c \rangle \big) \to Q \langle a, c \rangle$

Using co-continuity, we can pull the coend out:

$\int_{a, c, b} \big( S \langle a, b \rangle \times P \langle b, c \rangle \to Q \langle a, c \rangle \big)$

We then curry the product:

$\int_{a, c, b} \big( S \langle a, b \rangle \to (P \langle b, c \rangle \to Q \langle a, c \rangle ) \big)$

and re-arrange the ends:

$\int_{a, b} \big( S \langle a, b \rangle \to (\int_c P \langle b, c \rangle \to Q \langle a, c \rangle ) \big)$

We conclude that the right Kan lift is given by the formula:

$(\text{Rift}_P Q) \langle a, b \rangle = \int_c (P \langle b, c \rangle \to Q \langle a, c \rangle )$

What we did is a pretty standard calculation of a mapping out of a profunctor composition. We pull out the coend to turn it into an end, and then we curry the product.

A right Kan lift can be defined in a double category (actually, all we need is the horizontal=bicategorical part of it) using the counit 2-cell:

satisfying the universal property: Any 2-cell of the same shape as the counit uniquely factorizes through the counit:

Tannakian Reconstruction

We can now see that, in $\mathbb{P}rof$ , the left hand side of the Tannakian formula is the right Kan lift of the evaluation profunctor along itself:

$(\text{Rift}_E E) \langle b, a \rangle = \int_{\hat F \colon \hat A} \mathbf{Set}( E \langle a, \hat F \rangle, E \langle b, \hat F \rangle) \cong \int_{\hat F \colon \hat A} \mathbf{Set}( \hat F a, \hat F b)$

In a Yoneda equipment, the evaluation profunctor is the companion to the Yoneda functor, so we can replace $\text{Rift}_E E$ with $\text{Rift}_{y_*} y_*$ .

Using the definition of the Right Kan lift as a right adjoint to postcomposition we have, for any $S$ :

$(S \odot y_* \Rightarrow y_*) \cong (S \Rightarrow \text{Rift}_{y_*} y_*)$

In a proarrow equipment, the companion $y_*$ has a right adjoint, the conjoint $y^*$ . Graphically, this lets us bend the arrows in the diagram:

We get:

$(S \Rightarrow \text{Rift}_{y_*} y_*) \cong (S \odot y_* \Rightarrow y_*) \cong (S \Rightarrow {y_*} \odot y^*)$

Since $S$ is arbitrary, we can use the Yoneda lemma (the bicategorical version) to conclude that:

$\text{Rift}_{y_*} y_* \cong {y_*} \odot y^*$

Finally, in a Yoneda equipment we postulate the analog of the full-faithfullness of the Yoneda embedding:

$1 \cong y_* \odot y^*$

The Tannakian reconstruction in a Yoneda equipment can therefore be written as:

$\text{Rift}_{y_*} y_* \cong 1$

In a profunctor equipment, the unit on the right hand side is the hom-profunctor $A(b, a)$ .

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

Bartosz Milewski's Programming Cafe