2026-07-20T05:31:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23645 2025-10-27T10:30:35Z ddc:004 open_access

Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory Mimram, Samuel Oleon, Émile homotopy type theory polygraph Tietze transformation coherence Polygraphs play a fundamental role in algebra, geometry, and computer science, by generalizing group presentations to higher-dimensional structures and encoding coherence for those. They have recently been adapted by Kraus and von Raumer to the setting of homotopy type theory, where they are useful to define and study higher inductive types. Here, we develop the theory of 1-dimensional polygraphs, which correspond to presentations of sets in homotopy type theory. This requires us to introduce a dedicated notion of Tietze transformation, generalizing their well-known counterpart in group theory: the equivalence generated by those transformations characterizes situations where two 1-polygraphs present the same set. We also show a homotopy transfer theorem, which provides a way to transport coherence structures from one 1-polygraph to another. This work lays the foundations for a general theory of polygraphs in arbitrary dimensions, which should be useful for instance to define and study coherent group presentations, allowing for synthetic (co)homology computations. Most of the results in the article have been formalized with the Agda proof assistant using the cubical HoTT library. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Samuel Mimram and Émile Oleon 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.30 urn:nbn:de:0030-drops-236456 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.30 eng https://creativecommons.org/licenses/by/4.0/legalcode