License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.16
URN: urn:nbn:de:0030-drops-180009
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18000/
Go to the corresponding LIPIcs Volume Portal

Mimram, Samuel

Categorical Coherence from Term Rewriting Systems

pdf-format:
LIPIcs-FSCD-2023-16.pdf (1 MB)

Abstract

The celebrated Squier theorem allows to prove coherence properties of algebraic structures, such as MacLane’s coherence theorem for monoidal categories, based on rewriting techniques. We are interested here in extending the theory and associated tools simultaneously in two directions. Firstly, we want to take in account situations where coherence is partial, in the sense that it only applies for a subset of structural morphisms (for instance, in the case of the coherence theorem for symmetric monoidal categories, we do not want to strictify the symmetry). Secondly, we are interested in structures where variables can be duplicated or erased. We develop theorems and rewriting techniques in order to achieve this, first in the setting of abstract rewriting systems, and then extend them to term rewriting systems, suitably generalized in order to take coherence in account. As an illustration of our results, we explain how to recover the coherence theorems for monoidal and symmetric monoidal categories.

BibTeX - Entry

@InProceedings{mimram:LIPIcs.FSCD.2023.16,
  author =	{Mimram, Samuel},
  title =	{{Categorical Coherence from Term Rewriting Systems}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18000},
  URN =		{urn:nbn:de:0030-drops-180009},
  doi =		{10.4230/LIPIcs.FSCD.2023.16},
  annote =	{Keywords: coherence, rewriting system, Lawvere theory}
}

Keywords: coherence, rewriting system, Lawvere theory
Collection: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Issue Date: 2023
Date of publication: 28.06.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI