The Sequent Calculus of Skew Monoidal Categories
Tarmo Uustalu, Niccolò Veltri and Noam Zeilberger
Abstract
Szlachanyi’s skew monoidal categories are a well-motivated variation
of monoidal categories in which the unitors and associator are not
required to be natural isomorphisms, but merely natural
transformations in a particular direction. We present a sequent
calculus for skew monoidal categories, building on the recent
formulation by one of the authors of a sequent calculus for the Tamari
order (skew semigroup categories). In this calculus, antecedents
consist of a stoup (an optional formula) followed by a context, and
the connectives behave like in the standard monoidal sequent calculus
except that the left rules may only be applied in stoup position. We
prove that this calculus is sound and complete with respect to
existence of maps in the free skew monoidal category, and moreover
that it captures equality of maps once a suitable equivalence relation
is imposed on derivations. We then identify a subsystem of focused
derivations and establish that it contains exactly one canonical
representative from each equivalence class. This coherence theorem
leads directly to simple procedures for deciding equality of maps in
the free skew monoidal category and for enumerating any homset without
duplicates (in particular, for deciding existence of a map). Finally,
and in the spirit of Lambek’s work, we describe the close connection
between this proof-theoretic analysis and Bourke and Lack’s recent
characterization of skew monoidal categories as left representable
skew multicategories.
Agda code for the MFPS18 version of the paper
The formalization uses Agda 2.5.3 and Agda standard library 0.14.
The file Everything.agda contains the whole formalization.
Agda code for the extended version of the paper
The formalization uses Agda 2.5.3 and Agda standard library 0.14.
It also type-checks using Agda 2.6.0 and Agda standard library 0.16.
The file Everything.agda contains the whole formalization.