Rewriting in Gray categories with applications to coherence

TL;DR

This paper extends rewriting theory to Gray categories, enabling systematic coherence proofs for complex categorical structures through finite rewriting systems and an adapted Squier's theorem.

Contribution

It develops rewriting theory for Gray categories and precategories, proving coherence via finite systems and extending Squier's theorem to this setting.

Findings

Finite rewriting systems in precategories have finitely many critical pairs.

Convergent rewriting systems imply coherence, ensuring equality of parallel 3-cells.

Applied to structures like monoids, adjunctions, and Frobenius monoids in Gray categories.

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 include Gray categories as particular cases, and are adapted to mechanized computations. 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, Frobenius monoids.