The sequent calculus of skew monoidal categories
From MaRDI portal
Publication:5014602
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 2134022 (Why is no real title available?)
- scientific article; zbMATH DE number 3179491 (Why is no real title available?)
- scientific article; zbMATH DE number 4122189 (Why is no real title available?)
- scientific article; zbMATH DE number 7204452 (Why is no real title available?)
- scientific article; zbMATH DE number 3316072 (Why is no real title available?)
- scientific article; zbMATH DE number 3367095 (Why is no real title available?)
- scientific article; zbMATH DE number 3385867 (Why is no real title available?)
- A new constructive logic: classic logic
- A sequent calculus for a semi-associative law
- Associahedra, Tamari lattices and related structures. Tamari memorial Festschrift
- Coherence for skew-monoidal categories
- Deductive systems and categories
- Free skew monoidal categories
- Homotopy of operads and Grothendieck-Teichmüller groups. Part 2: The applications of (rational) homotopy theory methods
- Logic Programming with Focusing Proofs in Linear Logic
- Monoïdes préordonnés et chaînes de Malcev
- On MacLane's conditions for coherence of natural associativities, commutativities, etc
- Representable multicategories
- Skew monoidal categories and skew multicategories
- Skew monoidales, skew warpings and quantum categories
- Skew-closed categories
- Skew-monoidal categories and bialgebroids.
- The Catalan simplicial set
- The Mathematics of Sentence Structure
- The sequent calculus of skew monoidal categories
- Triangulations, orientals, and skew monoidal categories
- Untersuchungen über das logische Schliessen. I
Cited in
(10)- Proof Theory of Partially Normal Skew Monoidal Categories
- The sequent calculus of skew monoidal categories
- Skew monoidal categories and skew multicategories
- Free skew monoidal categories
- A practical type theory for symmetric monoidal categories
- Maximally multi-focused proofs for skew non-commutative \texttt{MILL}
- Coherence for skew-monoidal categories
- Remarks on units of skew monoidal categories
- Coherence via focusing for symmetric skew monoidal categories
- Proof theory of skew non-commutative \texttt{MILL}
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)
