{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T00:40:55Z","timestamp":1790296855710,"version":"4.1.0"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T00:00:00Z","timestamp":1669075200000},"content-version":"unspecified","delay-in-days":205,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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\u2019s 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.<\/jats:p>","DOI":"10.1017\/s0960129522000299","type":"journal-article","created":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T04:41:46Z","timestamp":1669092106000},"page":"574-647","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Rewriting in Gray categories with applications to coherence"],"prefix":"10.1017","volume":"32","author":[{"given":"Simon","family":"Forest","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0767-2569","authenticated-orcid":false,"given":"Samuel","family":"Mimram","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,11,22]]},"reference":[{"key":"S0960129522000299_ref11","volume-title":"Coherence for Tricategories","volume":"558","author":"Gordon","year":"1995"},{"key":"S0960129522000299_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061280"},{"key":"S0960129522000299_ref23","unstructured":"Makkai, M. (2005). The word problem for computads. Available on the author\u2019s web page http:\/\/www.math.mcgill.ca\/makkai\/."},{"key":"S0960129522000299_ref6","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/230\/03337"},{"key":"S0960129522000299_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(03)00069-0"},{"key":"S0960129522000299_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525902.011"},{"key":"S0960129522000299_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(94)00043-I"},{"key":"S0960129522000299_ref13","first-page":"420","article-title":"Higher-dimensional categories with finite derivation type","volume":"22","author":"Guiraud","year":"2009","journal-title":"Theory and Applications of Categories"},{"key":"S0960129522000299_ref30","doi-asserted-by":"publisher","DOI":"10.1063\/1.1788852"},{"key":"S0960129522000299_ref33","unstructured":"Weber, M. (2009). Free products of higher operad algebras. arXiv preprint arXiv:0909.4722."},{"key":"S0960129522000299_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(87)90129-0"},{"key":"S0960129522000299_ref32","unstructured":"Thue, A. (1914). Probleme \u00fcber Ver\u00e4nderungen von Zeichenreihen nach gegebenen Regeln, vol. 10."},{"key":"S0960129522000299_ref16","unstructured":"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\u2013238."},{"key":"S0960129522000299_ref24","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(2:1)2014"},{"key":"S0960129522000299_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511600579"},{"key":"S0960129522000299_ref2","volume-title":"Term Rewriting and All that","author":"Baader","year":"1999"},{"key":"S0960129522000299_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139542333"},{"key":"S0960129522000299_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90175-9"},{"key":"S0960129522000299_ref5","unstructured":"Barr, M. and Wells, C. (2005). Topos, Triples and Theories."},{"key":"S0960129522000299_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S096012951100065X"},{"key":"S0960129522000299_ref9","unstructured":"Delpeuch, A. and Vicary, J. (2018). Normalization for planar string diagrams and a quadratic equivalence algorithm. arXiv preprint arXiv:1804.07832."},{"key":"S0960129522000299_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90054-W"},{"key":"S0960129522000299_ref18","doi-asserted-by":"crossref","unstructured":"Knuth, D. E. and Bendix, P. B. (1970). Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"S0960129522000299_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(76)90013-X"},{"key":"S0960129522000299_ref15","first-page":"1","article-title":"Polygraphs of finite derivation type","author":"Guiraud","year":"2016","journal-title":"Mathematical Structures in Computer Science"},{"key":"S0960129522000299_ref10","volume-title":"Coherence for Frobenius pseudomonoids and the geometry of linear proofs","author":"Dunn","year":"2016"},{"key":"S0960129522000299_ref3","unstructured":"Bar, K. , Kissinger, A. and Vicary, J. (2016). Globular: an online proof assistant for higher-dimensional rewriting. In: LIPIcs, vol. 52, 34:1\u201334:11."},{"key":"S0960129522000299_ref22","article-title":"Natural associativity and commutativity","volume":"49","author":"MacLane","year":"1963","journal-title":"Rice Institute Pamphlet-Rice University Studies"},{"key":"S0960129522000299_ref25","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2008.v10.n1.a7"},{"key":"S0960129522000299_ref4","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005147"},{"key":"S0960129522000299_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-7954(96)80019-2"},{"key":"S0960129522000299_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BF01456932"},{"key":"S0960129522000299_ref31","volume-title":"Cambridge Tracts in Theoretical Computer Science","volume":"55","year":"2003"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000299","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,20]],"date-time":"2022-12-20T08:13:39Z","timestamp":1671524019000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000299\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["S0960129522000299"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000299","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}