Categorification, term rewriting and the Knuth–Bendix procedure

An axiomatization of a finitary, equational universal algebra by a convergent term rewrite system gives rise to a finite, coherent categorification of the algebra.