Abstract: I motivate a variation (due to K. Szlach'{a}nyi) 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.
Recommendations
- The sequent calculus of skew monoidal categories
- The sequent calculus of skew monoidal categories
- Proof Theory of Partially Normal Skew Monoidal Categories
- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
- Skew monoidal categories and skew multicategories
Cited in
(15)- Skew monoidal categories and skew multicategories
- Remarks on units of skew monoidal categories
- Free skew monoidal categories
- Coherence of associativity in categories with multiplication
- Eilenberg-Kelly reloaded
- The sequent calculus of skew monoidal categories
- Coherence via focusing for symmetric skew monoidal categories
- A sequent calculus for a semi-associative law
- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
- A practical type theory for symmetric monoidal categories
- The sequent calculus of skew monoidal categories
- Proof Theory of Partially Normal Skew Monoidal Categories
- On monads and warpings
- Coherence for monoidal groupoids in HoTT
- Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories
This page was built for publication: Coherence for skew-monoidal categories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4995162)
