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.

The notion of pasting diagram is central in the study of strict ω -categories: it encodes a collection of morphisms for which the composition is defined unambiguously. As such, we expect that a pasting diagram itself describes an ω-category which is freely generated by the cells constituting it. In practice, it seems very difficult to characterize this notion in full generality and various definitions have been proposed with the aim of being reasonably easy to compute with, and including common examples (e.g. cubes or orientals). One of the most tractable such structure is parity complexes, which uses sets of cells in order to represent the boundaries of a cell. In this work, we first show that parity complexes do not satisfy the aforementioned freeness property by providing a mechanized proof in Agda. Then, we propose a new formalism that satisfies the freeness property and which can be seen as a corrected version of parity complexes.