A layout algorithm for higher-dimensional string diagrams
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916132139565056 |
|---|---|
| author | Tataru, Calin Vicary, Jamie |
| author_facet | Tataru, Calin Vicary, Jamie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2305_06938 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | A layout algorithm for higher-dimensional string diagrams Tataru, Calin Vicary, Jamie Category Theory 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. |
| title | A layout algorithm for higher-dimensional string diagrams |
| topic | Category Theory |
| url | https://arxiv.org/abs/2305.06938 |