2 Search Results for "Guiraud, Yves"

Document
DOI: 10.4230/LIPIcs.FSCD.2025.30
Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory

Authors: Samuel Mimram and Émile Oleon

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{mimram_et_al:LIPIcs.FSCD.2025.30,
  author =	{Mimram, Samuel and Oleon, \'{E}mile},
  title =	{{Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.30},
  URN =		{urn:nbn:de:0030-drops-236456},
  doi =		{10.4230/LIPIcs.FSCD.2025.30},
  annote =	{Keywords: homotopy type theory, polygraph, Tietze transformation, coherence}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.223
A Homotopical Completion Procedure with Applications to Coherence of Monoids

Authors: Yves Guiraud, Philippe Malbos, and Samuel Mimram

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
One of the most used algorithm in rewriting theory is the Knuth-Bendix completion procedure which starts from a terminating rewriting system and iteratively adds rules to it, trying to produce an equivalent convergent rewriting system. It is in particular used to study presentations of monoids, since normal forms of the rewriting system provide canonical representatives of words modulo the congruence generated by the rules. Here, we are interested in extending this procedure in order to retrieve information about the low-dimensional homotopy properties of a monoid. We therefore consider the notion of coherent presentation, which is a generalization of rewriting systems that keeps track of the cells generated by confluence diagrams. We extend the Knuth-Bendix completion procedure to this setting, resulting in a homotopical completion procedure. It is based on a generalization of Tietze transformations, which are operations that can be iteratively applied to relate any two presentations of the same monoid. We also explain how these transformations can be used to remove useless generators, rules, or confluence diagrams in a coherent presentation, thus leading to a homotopical reduction procedure. Finally, we apply these techniques to the study of some examples coming from representation theory, to compute minimal coherent presentations for them: braid, plactic and Chinese monoids.
Cite as

Yves Guiraud, Philippe Malbos, and Samuel Mimram. A Homotopical Completion Procedure with Applications to Coherence of Monoids. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 223-238, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{guiraud_et_al:LIPIcs.RTA.2013.223,
  author =	{Guiraud, Yves and Malbos, Philippe and Mimram, Samuel},
  title =	{{A Homotopical Completion Procedure with Applications to Coherence of Monoids}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{223--238},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.223},
  URN =		{urn:nbn:de:0030-drops-40649},
  doi =		{10.4230/LIPIcs.RTA.2013.223},
  annote =	{Keywords: higher-dimensional rewriting, presentation of monoid, Knuth-Bendix completion, Tietze transformation, low-dimensional homotopy for monoids, coherence}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2013

  • Refine by Author
  • 2 Mimram, Samuel
  • 1 Guiraud, Yves
  • 1 Malbos, Philippe
  • 1 Oleon, Émile

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Constructive mathematics

  • Refine by Keyword
  • 2 Tietze transformation
  • 2 coherence
  • 1 Knuth-Bendix completion
  • 1 higher-dimensional rewriting
  • 1 homotopy type theory
  • Show More...

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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact