A layout algorithm for higher-dimensional string diagrams

TL;DR

This work introduces a new categorical tool called injectification, which lifts a functorial factorization system on a category to diagrams over that category, and shows that implementing this recursively in the category of finite posets allows us to systematically generate the necessary constraints.

Abstract

The algebraic zigzag construction has recently been introduced as a combinatorial foundation for a higher dimensional notion of string diagram. For use in a proof assistant, a layout algorithm is required to determine the optimal rendering coordinates, across multiple projection schemes including 2D, 3D, and 4D. For construction of these layouts, a key requirement is to determine the linear constraints which the geometrical elements must satisfy in each dimension. Here we introduce a new categorical tool called injectification, which lifts a functorial factorization system on a category to diagrams over that category, and we show that implementing this recursively in the category of finite posets allows us to systematically generate the necessary constraints. These ideas have been implemented as the layout engine of the proof assistant homotopy.io, enabling attractive and practical visualisations of complex higher categorical objects.

Figures (9)

• Figure 1: Example of a 2-diagram in homotopy.io.
• Figure 2: Example of a 3-diagram in homotopy.io.
• Figure 3: An interleaving of $\color{red}f : \mathbf{3} \to \mathbf{4}$ in $\mathbf{\Delta}$ going up, and $\color{blue}\mathop{\mathrm{\mathsf{R}}}\nolimits f : \mathbf{5} \to \mathbf{4}$ in $\boldsymbol{\nabla}$ going down.
• Figure 4: A zigzag map $f : X \to Y$ with the singular slices in red and regular slices in blue.
• Figure 5: A layout for a zigzag.

Theorems & Definitions (18)

• Definition 1
• Definition 2
• Definition 3
• Example 4
• Example 5
• Definition 6
• Proposition 7
• proof
• Definition 8
• Example 9