A cubical Squier's theorem

Convergent rewriting systems are well-known tools in the study of the word-rewriting problem. In particular, a presentation of a monoid by a finite convergent rewriting system gives an algorithm to decide the word problem for this monoid. Squier proved that there exists a finitely presented monoid whose word problem was decidable but which did not admit a finite convergent presentation. To do so, Squier constructed, for any convergent presentation $(G,R)$ of a monoid $M$, a set of syzygies $S$ corresponding to relations between the relations. This construction was later extended into the construction of a polygraphic resolution $\Sigma$ of $M$, whose first dimensions coincide with Squier's construction $(G,R,S)$. However, the construction of the polygraphic resolution has proved to be too complicated to be effectively computed on non-trivial examples. Cubical categories appear to be a promising framework where Squier's theorem and the construction of the polygraphic resolution would be more straightforward. This paper is the first step towards this goal. We start by defining the notion of $(2,k)$-cubical categories. We then adapt some classical notions of word rewriting to this cubical setting. Finally, we express and prove a cubical version of Squier's theorem.