Document Open Access Logo

Coherence of Gray Categories via Rewriting

Authors Simon Forest, Samuel Mimram

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.15.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Simon Forest
  • LIX, École Polytechnique, France
Samuel Mimram
  • LIX, École Polytechnique, France

Cite AsGet BibTex

Simon Forest and Samuel Mimram. Coherence of Gray Categories via Rewriting. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.15

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • rewriting
  • coherence
  • Gray category
  • polygraph
  • pseudomonoid
  • precategory

Metrics

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

References

  1. Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. In LIPIcs, volume 52, pages 34:1-34:11, 2016. URL: http://arxiv.org/abs/1612.01093.
  2. Krzysztof Bar and Jamie Vicary. Data structures for quasistrict higher categories. In Logic in Computer Science (LICS), 32nd Annual Symposium on, pages 1-12. IEEE, 2017. URL: http://arxiv.org/abs/1610.06908.
  3. Albert Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical computer science, 115(1):43-62, 1993. Google Scholar
  4. Lawrence Dunn and Jamie Vicary. Coherence for frobenius pseudomonoids and the geometry of linear proofs. Preprint, 2016. URL: http://arxiv.org/abs/1601.05372.
  5. François Foltz, Christian Lair, and GM Kelly. Algebraic categories with few monoidal biclosed structures or none. Journal of Pure and Applied Algebra, 17(2):171-177, 1980. Google Scholar
  6. Robert Gordon, Anthony John Power, and Ross Street. Coherence for tricategories, volume 558. American Mathematical Soc., 1995. Google Scholar
  7. John Walker Gray. Formal category theory: adjointness for 2-categories, volume 391. Springer, 2006. Google Scholar
  8. Yves Guiraud and Philippe Malbos. Higher-dimensional categories with finite derivation type. Theory and Applications of Categories, 22(18):420-478, 2009. Google Scholar
  9. Yves Guiraud and Philippe Malbos. Polygraphs of finite derivation type. Mathematical Structures in Computer Science, pages 1-47, 2016. URL: http://arxiv.org/abs/1402.2587.
  10. Yves Guiraud, Philippe Malbos, and Samuel Mimram. A homotopical completion procedure with applications to coherence of monoids. In RTA-24th International Conference on Rewriting Techniques and Applications, volume 21, pages 223-238, 2013. Google Scholar
  11. Nick Gurski. Coherence in three-dimensional category theory, volume 201. Cambridge Univ. Press, 2013. Google Scholar
  12. Aleks Kissinger and Jamie Vicary. Semistrict n-categories via rewriting. Proceedings of the first workshop on Higher-Dimensional Rewriting and Applications, 2015. Google Scholar
  13. Donald E Knuth and Peter B Bendix. Simple word problems in universal algebras. In Computational problems in abstract algebra, pages 263-297, 1970. Google Scholar
  14. Stephen Lack. A coherent approach to pseudomonads. Advances in Math., 152(2):179-202, 2000. Google Scholar
  15. Yves Lafont. Towards an algebraic theory of boolean circuits. Journal of Pure and Applied Algebra, 184(2):257-310, 2003. Google Scholar
  16. Samuel Mimram. Towards 3-Dimensional Rewriting Theory. Logical Methods in Computer Science, 10(1):1–47, 2014. URL: http://arxiv.org/abs/1403.4094.
  17. Craig C Squier, Friedrich Otto, and Yuji Kobayashi. A finiteness condition for rewriting systems. Theoretical Computer Science, 131(2):271-294, 1994. Google Scholar
  18. Ross Street. Categorical structures. Handbook of algebra, 1:529-577, 1996. Google Scholar
  19. Terese. Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  20. Dominic Verdon. Coherence for braided and symmetric pseudomonoids. Preprint, 2017. URL: http://arxiv.org/abs/1705.09354.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact