Previously: Profunctor Equipment in Haskell.

The major advantage of string diagrams is that they provide surpisingly 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).