Matrices of Categories, in 3D String Diagrams

Christian Williams

Tue Oct 17 2023

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.