A Categorical Framework for Coherence Theorems

Categories with coherently associative, commutative, and distributive products encapsulate higher algebraic structures throughout mathematics: for instance, in homotopy theory, they are the inputs to May’s infinite loop space machines [6, 7], Segal’s $K$-theory [10], and multifunctorial, multiplicative, and/or equivariant analogues of these by Elmendorf–Mandell [1], Guillou–May–Merling–Osorno [2, 3, 4], and Yau [11]. In ongoing work, we establish a general categorical approach to proving Mac Lane-like coherence theorems versatile enough to incorporate (weak) distributivity laws, module and algebra categories, bicategories, and the higher arity twisted products that appear in equivariant settings. Building on Mac Lane’s original proof of his coherence theorem for (symmetric) monoidal categories [5] and Rubin’s coherence theorem for his equivariant normed symmetric monoidal categories [8], we employ tools from combinatorics, logic, and rewriting theory such as Newman’s Diamond Lemma [9] to solve categorical normalization problems on the universal parameter categories representing categorical structures of interest. Our approach clarifies the necessary coherence axioms and invariants. We aim to leverage our work to simplify the characterization of bimonoidal categorical input to Yau’s multifunctorial equivariant algebraic $K$-theory.