Rewriting modulo in diagrammatic algebras and application to categorification

We develop a rewriting theory modulo suitable for higher linear structures. In particular, the theory is suited for diagrammatic algebras as they appear in categorification, representation theory and quantum topology. As an application, we use the theory to prove the basis conjecture of a certain super-2-category related to odd Khovanov homology. Our approach combines linear rewriting, higher rewriting and rewriting modulo. For diagrammatic algebras, the modulo rules typically capture a categorical property, such as pivotality. In the process, we revisit the foundations of these theories, including the notion of confluence. Other important tools include termination rules that depend on contexts, rewriting modulo invertible scalars, and a method to classify branchings modulo. This article includes an introduction to rewriting theory for non-experts.