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})).

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.