String Diagrams for Monoidal Double Categories

General
1

One application of 3D string diagrams is a visual language for monoidal double categories, seen as triple categories with one object and one horizontal morphism.

For example, \mathbb{R}\mathrm{el}: sets and functions, relations and entailments. A relation connects a product of sets to another product of sets, and this is essential to their expressiveness.

Let the vertical dimension be objects and tensor (sets and product), the horizontal dimension be h-morphisms and composition (relations and rel-comp), and the transversal (inner to outer) dimension be v-morphisms and composition (functions and fun-comp), with the whole diagram being a square (entailment).

So below, Q is a relation from \prod X to \prod Y, and R is a relation from \prod A to \prod B. Going outward, f:\prod X\to \prod A and g:\prod Y\to \prod B are functions; and finally, the whole cube is an entailment Q(\vec{x},\vec{y})\vdash R(f(\vec{x}),g(\vec{y})).

mon-dbl-cat
mon-dbl-cat1028Ă—547 15.7 KB

In particular, I think this “completes” graphical regular logic, by visualizing functions and entailments. @dspivak @epatters It would be great to discuss this sometime.

And in general, this applies to any monoidal double category: the above diagram could be a transformation of profunctors Q(\vec{x},\vec{y})\Rightarrow R(f(\vec{x}), g(\vec{y})).

So, there has been much exploration and application of monoidal double categories (and 2-categories) that can be visualized in this way. And these diagrams are barely any harder to draw (or code!) than monoidal categories – it’s just boxes in boxes.

Let me know what you think! Thanks.

3 Likes
2

Hi! Really interesting, as always. Would it be helpful if the arrows/functions/morphisms in the v dimension were denoted with some asymmetrical symbol, to indicate directionality (like a cap or a triangle or a trapezoid)? In the example diagram, for instance, it could be unclear that f is a function from X to A rather than A to X.

1 Like
3

Thanks! Yes, absolutely. I think it’s simple to draw them as outwards-pointing triangles.
(Of course, the graphic design can be improved.)

mdc-out
mdc-out1028Ă—547 17.1 KB

This is also essential for depicting companions and conjoints, by pulling either f or g from the side face to the inner face (where Q is); so yes the directed notation of arrows is very important. Thanks for clarifying.

1 Like
4

Is there either a coherence result for a topological version of triple category diagrams, or a combinatorial presentation of triple category diagrams? I.e. some result characterizing the free triple category on some generators?

5

If we draw string diagrams as exactly dual to ordinary diagrams, then I don’t think there is any need for topological definition or coherence theorem. By drawing beads as rectangles of any size, rather than points, there is never any need for strings to curve; and then their dual equivalence with ordinary diagrams is immediate.

As for a combinatorial representation, i.e. for programming purposes, I would be very happy to discuss. How hard is this, really, and could it be an extension of Semagrams?

6

Well, getting the combinatorial representation is at least a first step; it might not immediately lend itself to programming.

You can look at combinatorial definitions of undirected wiring diagram (which you might think of as morphisms of a free hypergraph category), or directed wiring diagrams (which you might think of as morphism of a free cartesian monoidal category), and see if there might be some analogous way to work things out? The tricky thing is that normally we view the inner boxes as the domain and the outer boxes as the codomain, but you also have “side boxes”, so we might have to do something more advanced than just an operad…

1 Like