2014/06/05 by Tarmo Uustalu · 3 citations
Computer Science · Mathematics · #Algebra over a field #Algebraic structures and combinatorial models #Associative property #Coherence (philosophical gambling strategy) #Commutative property #Homotopy and Cohomology in Algebraic Topology #Logic, programming, and type systems #Statement (logic) #Symmetric monoidal category #Uniqueness #Unital #cs.LO #cs.PL #math.CT
paper · pdf · doi:10.4204/eptcs.153.5
published in Electronic Proceedings in Theoretical Computer Science 153, 68-77 (Open Publishing Association) · In Proceedings MSFP 2014, arXiv:1406.1534
openalex publication_date 2014/06/05 · arxiv created 2014/06/09 · arxiv updated 2014/08/26 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05
I motivate a variation (due to K. Szlach'anyi) of monoidal categories called skew-monoidal categories where the unital and associativity laws are not required to be isomorphisms, only natural transformations. Coherence has to be formulated differently than in the well-known monoidal case. In my (to my knowledge new) version, it becomes a statement of uniqueness of normalizing rewrites. I present a proof of this coherence theorem and also formalize it fully in the dependently typed programming language Agda.