TY - JOUR
T1 - The Sequent Calculus of Skew Monoidal Categories
AU - Uustalu, Tarmo
AU - Veltri, Niccolò
AU - Zeilberger, Noam
PY - 2018
Y1 - 2018
N2 - Szlachányi'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 (a list of formulae), and the connectives unit and tensor behave like in intuitionistic non-commutative linear logic (the logic of monoidal categories) except that the left rules may only be applied in stoup position. We show the admissibility of two forms cut (stoup cut and context cut), and prove the calculus sound and complete with respect to existence of maps in the free skew monoidal category. We then introduce an equivalence relation on sequent calculus derivations and prove that there is a one-to-one correspondence between equivalence classes of derivations and maps in the free skew monoidal category. Finally, we identify a subcalculus of focused derivations, and establish that it contains exactly one canonical representative from each equivalence class. As an end result, we obtain simple algorithms both for deciding equality of maps in the free skew monoidal category and for enumerating any homset without duplicates, in particular, for deciding whether there is a map. We have formalized this development in the dependently typed programming language Agda.
AB - Szlachányi'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 (a list of formulae), and the connectives unit and tensor behave like in intuitionistic non-commutative linear logic (the logic of monoidal categories) except that the left rules may only be applied in stoup position. We show the admissibility of two forms cut (stoup cut and context cut), and prove the calculus sound and complete with respect to existence of maps in the free skew monoidal category. We then introduce an equivalence relation on sequent calculus derivations and prove that there is a one-to-one correspondence between equivalence classes of derivations and maps in the free skew monoidal category. Finally, we identify a subcalculus of focused derivations, and establish that it contains exactly one canonical representative from each equivalence class. As an end result, we obtain simple algorithms both for deciding equality of maps in the free skew monoidal category and for enumerating any homset without duplicates, in particular, for deciding whether there is a map. We have formalized this development in the dependently typed programming language Agda.
U2 - 10.1016/j.entcs.2018.11.017
DO - 10.1016/j.entcs.2018.11.017
M3 - Journal article
SN - 1571-0661
VL - 341
SP - 345
EP - 370
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -