We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Proof Theory of Partially Normal Skew Monoidal Categories

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.
Comments: In Proceedings ACT 2020, arXiv:2101.07888
Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)
Journal reference: EPTCS 333, 2021, pp. 230-246
DOI: 10.4204/EPTCS.333.16
Cite as: arXiv:2101.10487 [cs.LO]
  (or arXiv:2101.10487v1 [cs.LO] for this version)

Submission history

From: EPTCS [view email]
[v1] Tue, 26 Jan 2021 00:07:00 GMT (28kb,D)

Link back to: arXiv, form interface, contact.