May | 2026 | Bartosz Milewski's Programming Cafe

May 2026

Monthly Archive

May 23, 2026

Tabulation Tribulations

Posted by Bartosz Milewski under Category Theory | Tags: Category Theory, Double Categories, Profunctor Equipment, Profunctors |
Leave a Comment

Previously: Bending, Yanking, and Cartesian Squares in Double Categories.

We all know what a graph of a function is: it’s a set of pairs $(a, b)$ , where $b = f a$ . Similarly, a graph of a relation is a set of pairs where $b$ is related to $a$ .

A profunctor can be viewed as a proof-relevant relation. So a graph of a profunctor is a triple, which contains two objects and a proof, or a witness, that they are related. The witness in this case is any element of the set $J \langle a, b \rangle$ . If the set is empty, it means that the objects are unrelated.

Such triples form a category, which is often called the category of elements of a profunctor.

Given a profunctor $J \colon A^{op} \times B \to Set$ , an object in the category of elements is a triple $(a, j, b)$ . We interpret $j \in J \langle a, b \rangle$ as a witness that $a$ is related to $b$ .

A morphism in the category of elements between $(a, j, b)$ and $(a', j', b')$ is a pair of morphisms $(u \colon a \to a', v \colon b \to b')$ such that:

$J \langle a, v \rangle \,j = J \langle u, b' \rangle \, j'$

Here $J \langle a, v \rangle = J \langle id_a, v \rangle$ is the whiskering, or the lifting of a pair of morphisms, one of which is an identity, by the profunctor $J$ ; and similarly for $J \langle u, b' \rangle$ . We want the result, in both cases, to give us the same element of $J \langle a, b' \rangle$ — the witness that $a$ is related to $b'$ .

The analog of a graph of a profunctor in a double category is called a tabulation. A tabulation of a horizontal arrow $J \colon A \to B$ is a 0-cell $\langle J \rangle$ equipped with two projections. Think of these projections as extracting the two objects from the triple that we used in the definition of a graph of a profunctor. Their relation to $J$ is illustrated by the following 2-cell:

Let’s see how this works in $\mathbb{P}rof$ . Here we have a typical square that we’ve seen before, except that there is an invisible identity profunctor on the left — a hom-functor in the category $\langle J \rangle$ . The square tells us that for every morphism in $\langle J \rangle$ we can find a corresponding element of the profunctor $J$

Let’s pick two objects (triples) in $\langle J \rangle$ and a hom set between them:

$\langle J \rangle ((a, j, b), (a', j', b'))$

An element of this hom-set is a pair of morphisms $(u \colon a \to a', v \colon b \to b')$ . The 2-cell $\pi$ is a natural transformation whose components are:

$\pi_{(a, j, b)(a', j', b')} \colon \langle J \rangle ((a, j, b), (a', j', b')) \to J ( \pi_A (a, j, b), \pi_B (a', j', b'))$

Using our definitions, the argument of this mapping is a pair $(u, v)$ and the result is an element of the set $J(a, b')$ .

The mapping can be instantiated either by the lifting (whiskering) of $u$ or $v$ , both leading to the same result.

In a double category, we define a tabulation using its universal property. Just like a categorical product is universally defined by its mapping-in condition, so is a tabulation. However, since we are now working in a double category, besides the 1-dimensional mapping-in condition, we also need a 2-dimensional condition for 2-cells.

1-dimensional condition

What makes the projections projections is the mapping-in condition from some arbitrary 0-cell $X$ . We postulate that for any 0-cell $X$ that is equipped with two 1-cells $\phi_A$ and $\phi_B$ there is a unique factorization through the universal 2-cell $\pi$ :

In $\mathbb{P}rof$ , these 2-cells correspond to natural transformations:

$\phi_{x, x'} \colon X(x, x') \to J(\phi_A x, \phi_B x')$

$(\pi \circ id_{\phi'})_{x, x'} \colon X(x, x') \to J (\pi_A (\phi' x), \pi_B (\phi' x'))$

We can then define $\phi'$ , on objects, as:

$\phi' x = (\phi_A x, \phi_{x, x} id_x, \phi_B x)$

and acting on a morphism $f \colon x \to x'$ , as $(\phi_A f, \phi_B f)$ .

To summarize, the 1-dimensional condition lets us construct a vertical mapping $\phi' \colon X \to \langle J \rangle$ . All we have to provide is two vertical arrows and a 2-cell. But to complete the picture, we should be able to construct a 2-cell from another horizontal 1-cell, $H$ . For that we need a 2-dimensional universal condition.

2-dimensional condition

A 2-dimensional condition combines two instances of the one-dimensional condition. The second instance is another 0-cell $Y$ together with a projection $\psi$ , such that:

Using these two instances, we want to construct a mapping out of a horizontal 1-cell $H$ . There are two ways of combining these two instances on top of each other, and we postulate that the resulting 2-cells be equal:

In $\mathbb{P}rof$ , this corresponds to two natural transformations:

$\xi_{A\, x, y} \colon H(x, y) \to A(\phi_A x, \psi_A y)$
$\xi_{B\, x, y} \colon H(x, y) \to B(\phi_B x, \psi_B y)$

with the two composites equal:

$H(x, y) \to \int^{y'} A (\phi_A x, \psi_A y') \times J(\psi_A y', \psi_B y)$
$H(x, y) \to \int^{x'} J (\phi_A x, \phi_B x') \times B(\phi_B x', \psi_B y)$

The two-dimensional universal condition then statest that there is a unique 2-cell $\xi'$ :

such that both $\xi_A$ and $\xi_B$ factor through it. Here’s the first factorization:

In $\mathbb{P}rof$ , $\xi'$ is a natural transformation with a component:

$\xi'_{x, y} \colon H(x, y) \to \langle J \rangle (\phi' x, \psi' y)$

Substituting our definitions of $\phi'$ and $\psi'$ , we get as the target a pair of morphisms:

$(u \colon \phi_A x \to \psi_A y, v \colon \phi_B x \to \psi_B y)$

Given $h \in H (x, y)$ , we can construct such a pair as:

$( \xi_{A\, x, y} h, \xi_{B\, x, y} h)$

When followed by $id_{\pi_A}$ this produces $\xi_{A x, y}$ thus satisfying the 2-dimensional universal condition. The constraints on $\xi_A$ and $\xi_B$ ensure that the pair of morphisms is indeed a proper morphism in $\langle J \rangle$ .

The same argument works when we replace $A$ with $B$ .

From the practical point of view, the 2-dimensional condition lets us construct a mapping (a 2-cell) $\xi'$ from a horizontal 1-cell $H$ to $\langle J \rangle$ using a pair of mappings into $A$ and $B$ satisfying coherency conditions.

The advantage of the universal construction is that it avoids talking about individual sets or, for that matter, about the category of sets. It thus works out of the box for enriched profunctors and other exotic embodiments of double categories.

May 18, 2026

Bending, Yanking, and Cartesian Squares in Double Categories

Posted by Bartosz Milewski under Category Theory | Tags: Category Theory, Double Categories, Proarrow Equipment, Profunctor Equipment, Profunctors, String Diagrams |
Leave a Comment

Previously: Profunctor Equipment in Haskell.

The major advantage of string diagrams is that they provide surprisingly natural language for complex diagram manipulations. The fact that two traditional diagrams are equal can be often described as a permission to bend, yank, or pinch strings in particular ways. They provide visual and often tactile clues to our senses. This is even more helpful in the context of double categories and equipments.

Yanking

Consider the definition of a companion from the previous installment. It’s a horizontal arrow $B(f, 1)$ that is somehow related to a vertical arrow $f \colon A \to B$ . There are two 2-cells that illustrate this relation, but it’s not clear what their meaning is or how to use them.

It’s only when you start composing these cells that the computational aspect of companions emerges. The first condition is that the horizontal composite result in the identity $\eta \epsilon = id_f$ . Diagrammatically, we have:

You can visualize this as yanking the ends of the two arrows and letting the beads fall down.

The same trick can be done with vertical composition. The equation, $\epsilon \odot \eta = id_{B(1, f)}$ , is illustrated by the following diagrams:

This time we yank the arrows horizontally.

The two equalites for the conjoint arrows have analogous graphical interpretation resulting it this general rule that is valid in any proarrow equipment:

Any zig-zag in which the arrows flow in one direction and vertical arrows point downwards can be yanked.

The Spider Lemma

The yanking identities let us prove a very powerful lemma, which lets us bend arrows in many diagrams. The so called spider lemma states that the two diagrams below are isomorphic.

To prove it, we fist etablish two mappings: To get from the left diagram to the right one, we top it (vertically precompose) with the unit of the conjoint and the unit of the companion. This bends the arrows $f_1$ and $f_3$ and turns them into $A_1(1, f_1)$ and $A_3(f_3, 1)$ . Then we shove the two counits below it (vertically postcompose), to bend the arrows $g_1$ and $g_3$ .

To get from the right diagram to the left one, we do the analogous trick with horizontal pre/post composition. Finally, we prove that the two mappings are the inverse of each other by composing them and applying the yanking identities.

This is the spider lemma in its full glory, but we often specialize it to situations when one or more vertical arrows are identities. Then it lets us bend the remaining arrows.

Cartesian Squares

The workhorse of category theory is the universal construction. You define a new gadget by specifying its shape, and then pick the one through which all those shapes uniquely factor through. This is, for instance, how a categorical product is defined: The shape is a span with two fixed objects at its ends and a central object with arrows towards those objects. The product is the span through which all other spans factor through.

The same idea works in a double category, except that now we want to view it through string diagrams. We’ll illustrate it with the definition of a cartesian square.

Given a horizontal arrow $J$ and two vertical arrows $f$ and $g$ , a cartesian square defines a horizontal arrow $H = J(f, g)$ also called a restriction of $J$ along $f$ and $g$ . In the profunctor equipment $\mathbb{P}rof$ , this restriction is given by the hom-functor:

$\langle a, c \rangle \mapsto J(f a, g c)$

Since we want to avoid mentioning hom-sets, we’ll use a universal construction instead. Here’s the shape we are going to study:

We are given four 0-cells (the four areas), two vertical 1-cells $f$ and $g$ , and one horizontal cell $J$ . We want to find the universal one of $H$ and $\alpha$ . To this end we replace $H$ with a generic horizontal arrow $L \colon X \to Y$ , together with two new vertical arrows $h$ and $k$ that, just like $H$ and $\alpha$ before, are equipped with a 2-cell $\psi$ (see the left diagram below).

The universal condition states that any such shape can be uniquely factored out through the cartesian square $\alpha$ (see the right diagram below).

Visually, we are splitting the bead representing $\psi$ into two separate beads, the right one being the universal one. Or you may interpret it, right to left, as pinching together the two beads into one.

Most universal constructions in a double category look like this. You may easily figure out the definition of the opcartesian square by extending it on the right instead of on the left.

In $\mathbb{P}rof$ , this universal condition is a tautology, but in other double categories it may have computational meaning. It can be used, for instance, to compute a 2-cell $\psi'$ from $L$ to $J(f, g)$ over a pair of 1-cells $(h, k)$ , given the corresponding cartesian square $\alpha$ . All we need is to find a suitable $\psi$ from $L$ to $J$ over the composite $(f \circ h, g \circ k)$ .

May 16, 2026

Profunctor Equipment in Haskell

Posted by Bartosz Milewski under Category Theory, Haskell, Programming | Tags: Category Theory, Haskell, Profunctor Equipment |
[2] Comments

Previously: Profunctor Equipment.

To make things more palatable for programmers, I decided to provide a toy implementation of some of the equipments in Haskell. The advantage of this encoding is that it can be verified by the compiler, and I still trust the compiler more than I trust the AI.

A more adequate implementation would require a full-blown dependently typed language, but if we restrict ourselves to just a single category and work only with endo-functors and endo-profunctors, we can get at least some intuitions. If you want to see a more elaborate version, see the proarrows library by Sjoerd Visscher.

The only 0-cell I’ll be using is the Haskell category of types and functions. For vertical 1-cells I’ll use the standard library implementation of Functor, and for horizontal ones I’ll use Profunctor.

A 2-cell in $\mathbb{P}rof$ :

is implemented as a natural transformation:

type Cell f g h j = forall a c . h a c -> j (f a) (g c)

The forall serves as a universal quantifier.

The horizontal composition of such cells is given by:

hcomp :: (Functor f, Functor f', Functor g, Functor g'
         , Profunctor h, Profunctor j, Profunctor k) =>
    Cell f g h j -> Cell f' g' j k 
                 -> Cell (Compose f' f) (Compose g' g) h k
hcomp fg_hj fg_jk hac = dimap getCompose Compose $ fg_jk (fg_hj hac)

I used the library definition of functor composition:

newtype Compose f g a = Compose { getCompose :: f (g a) }

Vertical composition of cells uses a more elaborate profunctor composition:

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)

Profunctor composition is defined using a coend. In Haskell, we implement a coend:

$\int^x P \langle x, c\rangle \times Q \langle d, x \rangle$

as an existential type:

data Procompose p q d c where
  Procompose :: p x c -> q d x -> Procompose p q d c

Here, x is a type that’s not in the argument list, so it’s interpreted using the existential counterpart of forall.

This is the horizontal unit cell:

type Hunit p = Cell Identity Identity p p

hUnit :: Profunctor p => Hunit p
hUnit = dimap runIdentity Identity

and here’s its vertical counterpart:

type Vunit f a b = Cell f f (->) (->)

vUnit :: Functor f => Vunit f a b
vUnit = fmap

I used the library implementation of the Identity functor, and the type constructor (->) for the hom-profunctor–the unit of profunctor composition. The unit laws are satisfied up to isomorphism.

The companion and the conjoint are synonyms of the library types Costar and Star:

newtype Star f d c   = Star   { runStar   :: d -> f c }
newtype Costar f d c = Costar { runCostar :: f d -> c }

type Companion f d c = Costar f d c
type Conjoint f d c  = Star f d c

The companion unit and counit cells:

are given by, respectively:

type CompUnit f   = Cell Identity f (->) (Costar f)

compUnit :: Functor f => CompUnit f
compUnit h = Costar (fmap (h . runIdentity))

and

type CompCoUnit f = Cell f Identity (Costar f) (->)

compCoUnit :: Functor f => CompCoUnit f 
compCoUnit (Costar h) = Identity . h

Similarly for the conjoint:

type ConjUnit f   = Cell f Identity (->) (Star f)

conjUnit :: Functor f => ConjUnit f 
conjUnit h = Star  (fmap (Identity . h))

and:

type ConjCoUnit f = Cell Identity f (Star f) (->)

conjCoUnit :: Functor f => ConjCoUnit f 
conjCoUnit (Star h) = h . runIdentity

More advanced constructions would require the definition of categories internal to Hask and the use of dependent types.

Haskell code is available here.

Bartosz Milewski's Programming Cafe

May 2026

Tabulation Tribulations

1-dimensional condition

2-dimensional condition

Bending, Yanking, and Cartesian Squares in Double Categories

Yanking

The Spider Lemma

Cartesian Squares

Profunctor Equipment in Haskell

Top Posts

License

Blogroll

Follow Me

Archives