Proof Theory of Partially Normal Skew Monoidal Categories

zbMATH Open1477.18041arXiv2101.10487MaRDI QIDQ5019679FDOQ5019679

Authors: Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger 

Publication date: 10 January 2022

Abstract: The skew monoidal categories of Szlach'anyi are a weakening of monoidal categories where the three structural laws of left and right unitality and associativity are not required to be isomorphisms but merely transformations in a particular direction. In previous work, we showed that the free skew monoidal category on a set of generating objects can be concretely presented as a sequent calculus. This calculus enjoys cut elimination and admits focusing, i.e. a subsystem of canonical derivations, which solves the coherence problem for skew monoidal categories. In this paper, we develop sequent calculi for partially normal skew monoidal categories, which are skew monoidal categories with one or more structural laws invertible. Each normality condition leads to additional inference rules and equations on them. We prove cut elimination and we show that the calculi admit focusing. The result is a family of sequent calculi between those of skew monoidal categories and (fully normal) monoidal categories. On the level of derivability, these define 8 weakenings of the (unit,tensor) fragment of intuitionistic non-commutative linear logic.

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

Recommendations

• The sequent calculus of skew monoidal categories
• The sequent calculus of skew monoidal categories
• Skew monoidal categories and skew multicategories
• Coherence for skew-monoidal categories
• Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
• Remarks on units of skew monoidal categories
• Operadic categories and their skew monoidal categories of collections
• Skew-monoidal categories and bialgebroids.
• Free skew monoidal categories
• scientific article; zbMATH DE number 165319

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Categorical logic, topoi (03G30) Categorical aspects of linear logic (18M45)

Cites Work

• 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?)
• The Mathematics of Sentence Structure
• Skew monoidal categories and skew multicategories
• Skew-monoidal categories and bialgebroids.
• Logic Programming with Focusing Proofs in Linear Logic
• Coherence for associativity not an isomorphism
• Title not available (Why is that?)
• Skew monoidales, skew warpings and quantum categories
• Monads need not be endofunctors
• The sequent calculus of skew monoidal categories
• Skew-closed categories
• Braided skew monoidal categories
• Non‐commutative intuitionistic linear logic
• Triangulations, orientals, and skew monoidal categories
• Computer Science Logic
• Free skew monoidal categories
• Coherence for skew-monoidal categories
• Title not available (Why is that?)
• The Catalan simplicial set
• A sequent calculus for a semi-associative law
• A theory of linear typings as flows on 3-valent graphs

Cited In (8)

• Parsummable categories as a strictification of symmetric monoidal categories
• Eilenberg-Kelly reloaded
• Coherence via focusing for symmetric skew monoidal categories
• Free skew monoidal categories
• Coherence for skew-monoidal categories
• The sequent calculus of skew monoidal categories
• The sequent calculus of skew monoidal categories
• Proof theory of skew non-commutative \texttt{MILL}

This page was built for publication: Proof Theory of Partially Normal Skew Monoidal Categories

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