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.