Proof Theory of Partially Normal Skew Monoidal Categories

Reference. Proof Theory of Partially Normal Skew Monoidal Categories

Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger · EPTCS · 2021 · category-theory · DOI · arXiv

Cite

Cite as @uustalu-2021-proof (helia, typst) · \cite{uustalu-2021-proof} (LaTeX)

BibTeX

bibtex · 1 line

@article{uustalu-2021-proof, title={Proof Theory of Partially Normal Skew Monoidal Categories}, volume={333}, ISSN={2075-2180}, url={http://dx.doi.org/10.4204/eptcs.333.16}, DOI={10.4204/eptcs.333.16}, journal={Electronic Proceedings in Theoretical Computer Science}, publisher={Open Publishing Association}, author={Uustalu, Tarmo and Veltri, Niccolò and Zeilberger, Noam}, year={2021}, month=Feb, pages={230–246} }

hayagriva YAML (typst)

yaml · 18 lines

uustalu-2021-proof:
  type: article
  title: Proof Theory of Partially Normal Skew Monoidal Categories
  author:
  - Uustalu, Tarmo
  - Veltri, Niccolò
  - Zeilberger, Noam
  date: 2021-02
  page-range: 230-246
  url: http://dx.doi.org/10.4204/eptcs.333.16
  serial-number:
    doi: 10.4204/eptcs.333.16
    issn: 2075-2180
  parent:
    type: periodical
    title: Electronic Proceedings in Theoretical Computer Science
    publisher: Open Publishing Association
    volume: 333

Download: uustalu-2021-proof.bib · uustalu-2021-proof.yml

Cited by (2)

Deductive Systems and Coherence for Skew Prounital Closed Categories uustalu-2021-deductiveEPTCS · 2021

DOI · arXiv

Eilenberg-Kelly Reloaded uustalu-2020-eilenbergMFPS · 2020

DOI

Cites 27 works (4 here)

With notes (4)

Eilenberg-Kelly Reloaded uustalu-2020-eilenbergMFPS · 2020

DOI

A sequent calculus for a semi-associative law zeilberger-2019-aLMCS · 2019

We introduce a sequent calculus with a simple restriction of Lambek’s product rules that precisely captures the classical Tamari order, i.e., the partial order on fully-bracketed words (equivalently, binary trees) induced by a semi-associative law (equivalently, right rotation). We establish a focusing property for this sequent calculus (a strengthening of cut-elimination), which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. We then describe two main applications of the coherence theorem, including: 1. A new proof of the lattice property for the Tamari order, and 2. A new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice

𝑌_{𝑛}

DOI · arXiv

A theory of linear typings as flows on 3-valent graphs zeilberger-2018-aLICS · 2018

DOI · arXiv

The mathematics of sentence structure lambek58Amer. Math. Monthly · 1958

DOI

External (23)

Braided skew monoidal categories (2020)
Skew monoidal categories and skew multicategories (2018)
The Sequent Calculus of Skew Monoidal Categories (2018)
Free skew monoidal categories (2017)
Coherence for Skew-Monoidal Categories (2015)
Monads need not be endofunctors (2015)
The Catalan simplicial set (2014)
Triangulations, orientals, and skew monoidal categories (2014)
Skew-closed categories (2012)
Skew-monoidal categories and bialgebroids (2012)
Skew monoidales, skew warpings and quantum categories (2012)
Closed categories (nLab) (2009)
Focusing the Inverse Method for Linear Logic (2005)
Fibrations for abstract multicategories (2004)
Representable Multicategories (2000)
Logic Programming with Focusing Proofs in Linear Logic (1992)
Non‐commutative intuitionistic linear logic (1990)
Coherence for associativity not an isomorphism (1972)
Closed Categories (1966)
On MacLane's conditions for coherence of natural associativities, commutativities, etc (1964)
Natural associativity and commutativity (1963)
Catégories avec multiplication (1963)
On the calculus of syntactic types (1961)