Document Open Access Logo

Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory

Authors Samuel Mimram , Émile Oleon

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.30.pdf
  • Filesize: 1.15 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.30.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • homotopy type theory
  • polygraph
  • Tietze transformation
  • coherence

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Samuel Mimram and Émile Oleon. Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.30

Author Details

Samuel Mimram
  • LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau, France
Émile Oleon
  • LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau, France

Supplementary Materials

References

  1. Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, and Samuel Mimram. Polygraphs: from rewriting to higher categories. Cambridge University Press, 2025. Google Scholar
  2. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  3. Christopher J Dean, Eric Finster, Ioannis Markakis, David Reutter, and Jamie Vicary. Computads for weak ω-categories as an inductive type. Advances in Mathematics, 450, 2024. Google Scholar
  4. Yves Guiraud and Philippe Malbos. Identities among relations for higher-dimensional rewriting systems. In Operads 2009, volume 26 of Séminaires et congrès, pages 145-161. Société Mathématique de France, 2013. Google Scholar
  5. Yves Guiraud and Philippe Malbos. Polygraphs of finite derivation type. Mathematical Structures in Computer Science, 28(2):155-201, 2018. URL: https://doi.org/10.1017/S0960129516000220.
  6. Allen Hatcher. Algebraic Topology. Cambridge University Press, 2002. Google Scholar
  7. Simon Henry and Samuel Mimram. Tietze equivalences as weak equivalences. Applied Categorical Structures, 30(3):453-483, 2022. URL: https://doi.org/10.1007/S10485-021-09662-W.
  8. Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In Computational problems in abstract algebra, pages 263-297. Pergamon, 1970. Google Scholar
  9. Nicolai Kraus and Jakob von Raumer. Path spaces of higher inductive types in homotopy type theory. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785661.
  10. Nicolai Kraus and Jakob von Raumer. A rewriting coherence theorem with applications in homotopy type theory. Mathematical Structures in Computer Science, 32(7):982-1014, 2022. URL: https://doi.org/10.1017/S0960129523000026.
  11. Yves Lafont. A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier). Journal of Pure and Applied Algebra, 98(3):229-244, 1995. Google Scholar
  12. Yves Lafont, François Métayer, and Krzysztof Worytkiewicz. A folk model structure on omega-cat. Advances in Mathematics, 224(3):1183-1231, 2010. Google Scholar
  13. Samuel Mimram. Polygraphs in Agda. Software, (visited on 2025-06-23). URL: https://github.com/smimram/agda-polygraphs
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23666
  14. Samuel Mimram. Categorical coherence from term rewriting systems. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction (FSCD), volume 260 of LIPIcs, pages 16:1-16:17. Schloss Dagstuhl, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.16.
  15. Maxwell Herman Alexander Newman. On theories with a combinatorial definition of "equivalence". Annals of mathematics, 43(2):223-243, 1942. Google Scholar
  16. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential colimits in homotopy type theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 845-858. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394801.
  17. Craig C Squier, Friedrich Otto, and Yuji Kobayashi. A finiteness condition for rewriting systems. Theoretical Computer Science, 131(2):271-294, 1994. URL: https://doi.org/10.1016/0304-3975(94)90175-9.
  18. Heinrich Tietze. Über die topologischen Invarianten mehrdimensionaler Mannigfaltigkeiten. Monatshefte für Mathematik und Physik, 19:1-118, 1908. Google Scholar
  19. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  20. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Proceedings of the ACM on Programming Languages, 3:1-29, 2019. URL: https://doi.org/10.1145/3341691.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact