Tarmo Uustalu

 Reykjavik University 

Skew monoidal categories of Szlachányi are like monoidal categories except that the structural laws of unitality and associativity are only required to be natural transformations in a certain direction. One can similarly talk of skew variants of monoidal closed categories, closed categories (without the tensor but with the unit), prounital-closed categories (with just a “shadow” of the unit in a non-represented form), and also of partially normal skew X categories where partial normality means that some of the structural laws are required to be invertible. All of these arise naturally in various categorical contexts and also in computer science, in semantical applications, in particular around various constructions with monads and comonads.

Coherence for this type of categories with structure is not like Mac Lane’s for monoidal categories: it is far from trivial to analyze the homsets of the free skew monoidal category or, more generally, the free skew X category, over a set or a (multi)graph and interesting phenomena occur.

In this talk, I will explain how this problem can be approached with methods of structural proof theory. The idea is to identify a map of the free skew X category with an equivalence class of derivations in a suitable sequent calculus. Applying the technique of focusing, one then seeks to define a canonical representative for each equivalence class.

This is joint work with Niccolò Veltri (Tallinn University of Technology) and Noam Zeilberger (École Polytechnique).