A layout algorithm for higher-dimensional string diagrams

arXiv2305.06938MaRDI QIDQ6510069FDOQ6510069

Authors: Calin Tataru, Jamie Vicary 

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.

This page was built for publication: A layout algorithm for higher-dimensional string diagrams

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6510069)