2018_EJRNL_PP_TARMO_UUSTALU_1_pdf.pdf
Terbatas Dwi Ary Fuziastuti
» ITB
Terbatas Dwi Ary Fuziastuti
» ITB
Szlach´anyi’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.