A Categorical Framework for Coherence Theorems

Abstract

Categories with coherently associative, commutative, and distributive products encapsulate higher algebraic structures that model both pure mathematical objects and real-world phenomena. In ongoing joint work with Jonathan Rubin, we establish a general categorical framework for proving Mac Lane-like coherence theorems for such categories. Our framework is versatile enough to incorporate 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 and Rubin’s coherence theorem for his equivariant normed symmetric monoidal categories, we employ tools from combinatorics, logic, and rewriting theory such as Newman’s Diamond Lemma to solve categorical normalization problems on universal parameter categories representing the categorical structures of interest. Our approach clarifies the necessary coherence axioms and invariants and is ripe for applications and possible automation.