Matrices of Categories, in 3D String Diagrams

A span of categories \mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B} is equivalent to a matrix of categories \mathcal{R}(\mathrm{A,B}), i.e. a “displayed category” \mathcal{R}:\mathbb{A\times B}\to \mathbb{C}\mathrm{at}. This equivalence is the foundation of dependent category theory.

We introduce 3-dimensional string diagrams, here in the intercategory \mathrm{SpanCat}, and also the language of color syntax, which combines string diagrams and mathematical syntax. We see that in this language, the equivalence between spans and matrices of categories is “already built in”.

A span of categories can be drawn simply as a string.

The span determines a matrix of categories, by inverse image along \mathcal{R}\to \mathbb{A\times B}, via pullback.

In syntax, pullback corresponds to substitution; i.e. “plugging” the objects \mathrm{A,B} into \mathcal{R}, to determine the fiber category \mathcal{R}(\mathrm{A,B}).

Here’s the magic: we can use the string diagram as a dependent type! Just by writing the pair of objects in the colored areas of \mathbb{A} and \mathbb{B}, the diagram can be faithfully interpreted as the fiber category.

Yet so far this is only the objects; how do we see the morphisms? The hom of \mathbb{A} or \mathbb{B} (a profunctor) can be drawn as a downward “pointer string”. The hom of \mathcal{R} (a span of profunctors) can be drawn as a “bead” which connects the \mathcal{R} string to itself, along the homs of \mathbb{A} and \mathbb{B}.

So for each pair of objects there is a category \mathcal{R}(\mathrm{A,B}); now in the same way, for each pair of morphisms \mathrm{a}:\mathbb{A}(\mathrm{A_0,A_1}) and \mathrm{b}:\mathbb{B}(\mathrm{B_0,B_1}) there is a profunctor \vec{\mathcal{R}}(\mathrm{a,b}) from \mathcal{R}(\mathrm{A_0,B_0}) to \mathcal{R}(\mathrm{A_1,B_1}). This is given by pullback in \mathrm{Prof}, along the transformation which selects the pair (\mathrm{a,b}).

Again, this substitution can be written right on the string diagram! By plugging the pair \mathrm{a,b} into the hom-strings of \mathbb{A} and \mathbb{B}, the diagram represents the profunctor \vec{\mathcal{R}}(\mathrm{a,b}).

Since the profunctor is itself a dependent type, we can now go a level further, and substitute particular objects of \mathcal{R} on the strings, to determine the set of morphisms \vec{\mathcal{R}}(\mathrm{a,b})(R_0,R_1) which lie over (\mathrm{a,b}).

So, we can see the 2-dimensional data of a span of categories in full detail.

Now, the composition and identity of \mathcal{R} is 3-dimensional structure.

Composition in \mathcal{R} determines transformations \vec{\mathcal{R}}(\mathrm{a_1,b_1})\circ \vec{\mathcal{R}}(\mathrm{a_2,b_2})\Rightarrow \vec{\mathcal{R}}(\mathrm{a_1a_2,b_1b_2}). This means that for each composable pair in \mathbb{A\times B}, given a morphism r_1 over (\mathrm{a_1,b_1}) and a morphism r_2 over (\mathrm{a_2,b_2}), the composite r_1r_2 lies over the composite (\mathrm{a_1a_2,b_1b_2}).

The transformation can be drawn in the third visual dimension, from inner to outer.

Similarly for identities: given any object R: \mathcal{R}(\mathrm{A,B}), its identity \mathrm{id}.R lies over the identities (\mathrm{id.A, id.B}).

Finally, composition is associative and unital; the reader is invited to draw the equal pairs of cubes. All together, we have constructed a displayed category: a normal lax functor \mathcal{R}:\mathbb{A\times B}\to \mathbb{C}\mathrm{at}.

This idea expands to matrices of functors, profunctors, and transformations. Miraculously, the language of dependent categories can be completely visualized. The string diagram represents a general concept, and writing syntax determines a specific instance. This combines the intuition of imagery with the computation of syntax, and becomes especially powerful in three dimensions.

Thanks for reading! (This is just a brief introduction, to be expanded; let me know if something isn’t clear.) Looking forward to hearing your thoughts.

2 Likes

It took me a few tries to get the first sentence to type-check! I guess you mean a displayed category viewed as a normal lax double functor into the double category of profunctors.

Quick reports of places I got stuck in figuring out the 2-D syntax for the first time: I got briefly stuck wanting to draw a picture of a span of profunctors when you use that phrase, which isn’t necessary since you’re going to explain in more detail a moment later. I did have to write out what was going on to keep straight that R_0,R_1 are in \mathcal R(A_0,B_0) and \mathcal R(A_1,B_1) respectively, since you just refer to them as objects of \mathcal R. In retrospect, the fully decorated square works very well, though, because all of that information is explicitly displayed.

On the 3D business, I don’t understand whether in the exercise for the reader I’m supposed to be able to prove that composition is associative from the cubes I draw. If so I don’t understand how to tell that two cubes are equal. And I definitely groan and turn away at trying to figure out what exactly is represented by the last lovely picture.

Thanks for your thoughts!

Each of these diagrams is dual to the conventional diagrams - and that’s why “color syntax” works. In particular, the hom of \mathcal{R} is a span of profunctors:

Just as a profunctor consists of “arrows” (vertical/tight morphisms) between categories, a span of categories consists of “proarrows” (horizontal/loose morphisms) between categories, and a span of profunctors consists of “hetero-squares”. The language of \mathrm{SpanCat} is the underlying metalanguage of double categories.

The last image is a span of transformations, a general cube in \mathrm{SpanCat}. It is dual to the ordinary diagram - but in string diagrams it is easier to see both spans of profunctors, and to grasp its semantic meaning: a mapping of squares.

Let me know if this is clear; thanks!

As for associativity and unitality, these hold by definition that \mathcal{R} is a category over \mathbb{A\times B}.

How do you draw all these diagrams Christian?

I draw them in Notability on an iPad. It has a grid of points; you make lines with pen, and boxes with highlighter, then fill with color. You can then add text with math notation, but it has some glitches. This app has been enough to get by for now, but the whole process is way too slow and unsystematic.

We need a good drawing app. It can be extremely simple, but it does not exist yet. So my top priority, after putting the thesis on arXiV, is to connect with a programmer and get a bit of funding to make this - because all of the education and research in this language will be based on these drawings.

If you have ideas, let me know!

Well, Nathanael Arkor has the best proof of concept of a simple, effective drawing app for category theory in q.uiver.io. He might be worth talking to. But I think the actual functionalities would have limited overlap. That’s impressive that you’ve been able to get this far with Notability. homotopy.io is more closely related in its goals although I don’t really understand how to use it.

Nathanael also has a tool for drawing string diagrams specifically for double categories, although it is currently much more a prototype than quiver: GitHub - varkor/tangle: A modern string diagram editor for the web.

2 Likes