Kraus, N. (2023). A Rewriting Coherence Theorem with Applications in Homotopy Type Theory. Mathematical Structures in Computer Science, 32(7), 982-1014. https://doi.org/10.1017/S0960129523000026