The sequent calculus of skew monoidal categories

DOI10.1007/978-3-030-66545-6_11zbMATH Open1495.03073arXiv2003.05213OpenAlexW3011585936MaRDI QIDQ5014602FDOQ5014602

Tarmo Uustalu, Noam Zeilberger, Niccolò Veltri

Publication date: 8 December 2021

Published in: Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics (Search for Journal in Brave)

Abstract: 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, 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. 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. We have formalized this development in the dependently typed programming language Agda.

Full work available at URL: https://arxiv.org/abs/2003.05213

Recommendations

• The sequent calculus of skew monoidal categories
• Free skew monoidal categories
• Proof Theory of Partially Normal Skew Monoidal Categories
• Coherence for skew-monoidal categories
• Remarks on units of skew monoidal categories

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Monoidal categories, symmetric monoidal categories (18M05)

Cites Work

• Untersuchungen über das logische Schliessen. I
• Title not available (Why is that?)
• Representable multicategories
• On MacLane's conditions for coherence of natural associativities, commutativities, etc
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Associahedra, Tamari lattices and related structures. Tamari memorial Festschrift
• The Mathematics of Sentence Structure
• Skew monoidal categories and skew multicategories
• Skew-monoidal categories and bialgebroids.
• Title not available (Why is that?)
• Title not available (Why is that?)
• A new constructive logic: classic logic
• Logic Programming with Focusing Proofs in Linear Logic
• Deductive systems and categories
• Skew monoidales, skew warpings and quantum categories
• Monoïdes préordonnés et chaînes de Malcev
• Homotopy of Operads and Grothendieck–Teichmüller Groups
• The sequent calculus of skew monoidal categories
• Skew-closed categories
• Triangulations, orientals, and skew monoidal categories
• Free skew monoidal categories
• Coherence for Skew-Monoidal Categories
• The Catalan simplicial set
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (7)

• Coherence via focusing for symmetric skew monoidal categories
• Remarks on units of skew monoidal categories
• Maximally multi-focused proofs for skew non-commutative \texttt{MILL}
• Skew monoidal categories and skew multicategories
• Proof theory of skew non-commutative \texttt{MILL}
• Proof Theory of Partially Normal Skew Monoidal Categories
• A practical type theory for symmetric monoidal categories

This page was built for publication: The sequent calculus of skew monoidal categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5014602)