Talk by Niccolò Veltri: «Proof Theory of Skew Monoidal Categories»
For the next seminar of the proofs and algorithms pole of LIX on Monday, we are happy to welcome Niccolò Veltri, who will be telling us about the (truly delightful!) proof theory of skew monoidal categories and related structures.
Abstract: The skew monoidal categories of Szlachányi are a weakening of monoidal categories where the three structural laws of left and right unitality and associativity are not required to be isomorphisms but merely transformations in a particular direction. In this talk, we show that the free skew monoidal category on a set of generating objects can be concretely presented as a sequent calculus. This calculus enjoys cut elimination and admits focusing, i.e. a subsystem of canonical derivations, which solves the coherence problem for skew monoidal categories.
We also develop sequent calculi for partially normal skew monoidal categories, which are skew monoidal categories with one or more structural laws invertible. Each normality condition leads to additional inference rules and equations on them. We prove cut elimination and we show that the calculi admit focusing. The result is a family of sequent calculi between those of skew monoidal categories and (fully normal) monoidal categories. On the level of derivability, these define 8 weakenings of the (unit,tensor) fragment of intuitionistic non-commutative linear logic.
If time allows it, we briefly discuss the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew closed categories in turn are a weakening of the closed categories of Eilenberg and Kelly where no structural law is required to be invertible and the presence of a monoidal structure is not required.
Joint work with Tarmo Uustalu and Noam Zeilberger
The list of next seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/
The calendar of seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar.ics