  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.
