Over the recent years, the theory of rewriting has been extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to low-dimensional weak categories, and consider in details the first non-trivial case: presentations of tricategories. By a general result, those are equivalent to the stricter Gray categories, for which we introduce a notion of rewriting system, as well as associated tools: critical pairs, termination orders, etc. We show that a finite rewriting system admits a finite number of critical pairs and, as a variant of Newman's lemma in our context, that a convergent rewriting system is coherent, meaning that two parallel 3-cells are necessarily equal. This is illustrated on rewriting systems corresponding to various well-known structures in the context of Gray categories (monoids, adjunctions, Frobenius monoids). Finally, we discuss generalizations in arbitrary dimension.
@InProceedings{forest_et_al:LIPIcs.FSCD.2018.15, author = {Forest, Simon and Mimram, Samuel}, title = {{Coherence of Gray Categories via Rewriting}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {15:1--15:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.15}, URN = {urn:nbn:de:0030-drops-91855}, doi = {10.4230/LIPIcs.FSCD.2018.15}, annote = {Keywords: rewriting, coherence, Gray category, polygraph, pseudomonoid, precategory} }
Feedback for Dagstuhl Publishing