Skew Monoidal Categories and the Proof-theoretic Anatomy of Associativity (and Unitality)
Ecole Polytechnique
Abstract:
Based on joint work with Tarmo Uustalu and Niccolò Veltri.
The talk will survey a recent line of work, which takes a proof-theoretic
approach to solving the coherence problem(s) for skew monoidal categories
and related structures. I will begin by discussing the so-called Tamari
order on fully-bracketed words induced by a semi-associative law (AB)C <=
A(BC), and explain how a simple sequent calculus may account for some of
its fascinating properties, such as the fact that the set of
fully-bracketed words on n+1 letters forms a lattice Y_n under this order,
as well as a remarkable formula counting the number of intervals in Y_n.
Then I will recall the definition of skew monoidal categories, and explain
how a more refined sequent calculus may be used to solve two related
coherence problems: deciding equality of maps and enumerating homsets in
free skew monoidal categories. Finally, I will briefly discuss variations
of the sequent calculus capturing "partially skew" monoidal categories with
different normality conditions.