Abstract

The symmetric skew monoidal categories of Bourke and Lack are a weakening of Mac Lane’s symmetric monoidal categories where: the three structural laws of left and right unitality and associativity are not required to be invertible, they are merely natural transformations with a specific orientation; the structural law of symmetry is a natural isomorphism involving three objects rather than two. In this paper we study the structural proof theory of symmetric skew monoidal categories, progressing the project initiated by Uustalu et al. on deductive systems for categories with skew structure. We discuss three equivalent presentations of the free symmetric skew monoidal category on a set of generating objects: a Hilbert-style categorical calculus; a cut-free sequent calculus; a focused subsystem of derivations, corresponding to a sound and complete goal-directed proof search strategy for the cut-free sequent calculus. Focusing defines an effective normalization procedure for maps in the free symmetric skew monoidal category, as such solving the coherence problem for symmetric skew monoidal categories.