Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-25T08:42:48.810Z Has data issue: false hasContentIssue false
  • English
  • Français

Rewriting in Gray categories with applications to coherence

Published online by Cambridge University Press:  22 November 2022

Simon Forest  and
Samuel Mimram Open the ORCID record for Samuel Mimram [Opens in a new window]
Simon Forest
Affiliation:
LIX, École Polytechnique, Palaiseau, France
Samuel Mimram*
Affiliation:
LIX, École Polytechnique, Palaiseau, France
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which are adapted to mechanized computations and include Gray categories as particular cases. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed. We also extend Squier’s theorem to our context, showing that a convergent rewriting system is coherent, which means that any two parallel 3-cells are necessarily equal. This allows us to prove coherence results for several well-known structures in the context of Gray categories: monoids, adjunctions, and Frobenius monoids.

Keywords

RewritingcoherenceGray categorypolygraph
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 32 , Issue 5 , May 2022 , pp. 574 - 647
Check for updates
Copyright
© The Author(s), 2022. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Adámek, J. and Rosický, J. (1994). Locally Presentable and Accessible Categories, vol. 189, Cambridge University Press.CrossRefGoogle Scholar
Baader, F. and Nipkow, T. (1999). Term Rewriting and All that, Cambridge University Press.Google Scholar
Bar, K., Kissinger, A. and Vicary, J. (2016). Globular: an online proof assistant for higher-dimensional rewriting. In: LIPIcs, vol. 52, 34:1–34:11.Google Scholar
Bar, K. and Vicary, J. (2017). Data structures for quasistrict higher categories. In: 32nd Annual Symposium on Logic in Computer Science (LICS), IEEE, 1–12.CrossRefGoogle Scholar
Barr, M. and Wells, C. (2005). Topos, Triples and Theories.Google Scholar
Batanin, M. A. (1998). Computads for finitary monads on globular sets. Contemporary Mathematics 230 37–58.CrossRefGoogle Scholar
Burroni, A. (1993). Higher-dimensional word problems with applications to equational logic. Theoretical Computer Science 115 (1) 43–62.CrossRefGoogle Scholar
Dehn, M. (1911). Über unendliche diskontinuierliche gruppen. Mathematische Annalen 71 (1) 116–144.CrossRefGoogle Scholar
Delpeuch, A. and Vicary, J. (2018). Normalization for planar string diagrams and a quadratic equivalence algorithm. arXiv preprint arXiv:1804.07832.Google Scholar
Dunn, L. and Vicary, J. (2016). Coherence for Frobenius pseudomonoids and the geometry of linear proofs. Preprint.Google Scholar
Gordon, R., Power, J. and Street, R. (1995). Coherence for Tricategories, vol. 558, American Mathematical Society.Google Scholar
Gray, J. W. (1974). Formal Category Theory: Adjointness for 2-Categories, vol. 391, Springer.CrossRefGoogle Scholar
Guiraud, Y. and Malbos, P. (2009). Higher-dimensional categories with finite derivation type. Theory and Applications of Categories 22 (18) 420–478.Google Scholar
Guiraud, Y. and Malbos, P. (2012). Coherence in monoidal track categories. Mathematical Structures in Computer Science 22 (6) 931–969.CrossRefGoogle Scholar
Guiraud, Y. and Malbos, P. (2016). Polygraphs of finite derivation type. Mathematical Structures in Computer Science, 1–47.Google Scholar
Guiraud, Y., Malbos, P. and Mimram, S. (2013). A homotopical completion procedure with applications to coherence of monoids. In: RTA-24th International Conference on Rewriting Techniques and Applications, vol. 21, 223–238.Google Scholar
Gurski, N. (2013). Coherence in Three-Dimensional Category Theory, vol. 201, Cambridge University Press.CrossRefGoogle Scholar
Knuth, D. E. and Bendix, P. B. (1970). Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, 263–297.Google Scholar
Lafont, Y. (1992). Penrose diagrams and 2-dimensional rewriting. Applications of Categories in Computer Science 177 191–201.CrossRefGoogle Scholar
Lafont, Y. (1995). 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.CrossRefGoogle Scholar
Lafont, Y. (2003). Towards an algebraic theory of boolean circuits. Journal of Pure and Applied Algebra 184 (2) 257–310.CrossRefGoogle Scholar
MacLane, S. (1963). Natural associativity and commutativity. Rice Institute Pamphlet-Rice University Studies 49 (4).Google Scholar
Makkai, M. (2005). The word problem for computads. Available on the author’s web page http://www.math.mcgill.ca/makkai/.Google Scholar
Mimram, S. (2014). Towards 3-dimensional rewriting theory. Logical Methods in Computer Science 10 (1) 1–47.CrossRefGoogle Scholar
Métayer, F. (2008). Cofibrant objects among higher-dimensional categories. Homology, Homotopy and Applications 10 (1) 181–203.CrossRefGoogle Scholar
Squier, C. C. (1987). Word problems and a homological finiteness condition for monoids. Journal of Pure and Applied Algebra 49 (1–2) 201–217.CrossRefGoogle Scholar
Squier, C. C., Otto, F. and Kobayashi, Y. (1994). A finiteness condition for rewriting systems. Theoretical Computer Science 131 (2) 271–294.CrossRefGoogle Scholar
Street, R. (1976). Limits indexed by category-valued 2-functors. Journal of Pure and Applied Algebra 8 (2) 149–181.CrossRefGoogle Scholar
Street, R. (1996). Categorical structures. Handbook of Algebra 1 529–577.CrossRefGoogle Scholar
Street, R. (2004). Frobenius monads and pseudomonoids. Journal of Mathematical Physics 45 (10) 3930–3948.CrossRefGoogle Scholar
Terese. (2003). Term Rewriting Systems , Cambridge Tracts in Theoretical Computer Science, vol. 55, Cambridge University Press.Google Scholar
Thue, A. (1914). Probleme über Veränderungen von Zeichenreihen nach gegebenen Regeln, vol. 10.Google Scholar
Weber, M. (2009). Free products of higher operad algebras. arXiv preprint arXiv:0909.4722.Google Scholar