In category theory there are numerous coherence theorems (https://ncatlab.org/nlab/show/coherence+theorem). One example is the Mac Lane's coherence theorem for monoidal categories. This and probably others as well, I believe, can be formulated in the language of term rewriting (https://en.wikipedia.org/wiki/Rewriting).
What work has been done in the term rewriting theory related to coherence in category theory? Are there general results in the term rewriting theory from which various categorical coherence theorems follow?
There may be some advantages to the term rewriting formulation in practice too. For example, analogous to a monoidal category, one can define a pseudomonoid (also called a monoidale) internal to a monoidal 2-category. This should satisfy coherence similar to Mac Lanes's coherence, which will involve 2-cells rather than natural transformations. Some other similar coherences also can occur (see Pseudomodules, "general coherence theorem"). I think that all these should follow from one term rewriting result.
I am also interested in term rewriting for higher categorical coherence.