  Higher-dimensional rewriting systems are tools to analyse the structure of
formally reducing terms to normal forms, as well as comparing the different
reduction paths that lead to those normal forms. This higher structure can be
captured by finding a homotopy basis for the rewriting system. We show that the
basic notions of confluence and wellfoundedness are sufficient to recursively
build such a homotopy basis, with a construction reminiscent of an argument by
Craig C. Squier. We then go on to translate this construction to the setting of
homotopy type theory, where managing equalities between paths is important in
order to construct functions which are coherent with respect to higher
dimensions. Eventually, we apply the result to approximate a series of open
questions in homotopy type theory, such as the characterisation of the homotopy
groups of the free group on a set and the pushout of 1-types.
  This paper expands on our previous conference contribution "Coherence via
Wellfoundedness" (arXiv:2001.07655) by laying out the construction in the
language of higher-dimensional rewriting.
