ITU

The Sequent Calculus of Skew Monoidal Categories

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

View graph of relations

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.
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Volume341
Pages (from-to)345-370
ISSN1571-0661
DOIs
Publication statusPublished - 2018

Downloads

No data available

ID: 83637459