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.