Reference. Deductive Systems and Coherence for Skew Prounital Closed Categories

Cite

Cite as @uustalu-2021-deductive (helia, typst) · \cite{uustalu-2021-deductive} (LaTeX)
BibTeX
bibtex · 1 line
@article{uustalu-2021-deductive, title={Deductive Systems and Coherence for Skew Prounital Closed Categories}, volume={332}, ISSN={2075-2180}, url={http://dx.doi.org/10.4204/eptcs.332.3}, DOI={10.4204/eptcs.332.3}, journal={Electronic Proceedings in Theoretical Computer Science}, publisher={Open Publishing Association}, author={Uustalu, Tarmo and Veltri, Niccolò and Zeilberger, Noam}, year={2021}, month=Jan, pages={35–53} }
hayagriva YAML (typst)
yaml · 18 lines
uustalu-2021-deductive:
  type: article
  title: Deductive Systems and Coherence for Skew Prounital Closed Categories
  author:
  - Uustalu, Tarmo
  - Veltri, Niccolò
  - Zeilberger, Noam
  date: 2021-01
  page-range: 35-53
  url: http://dx.doi.org/10.4204/eptcs.332.3
  serial-number:
    doi: 10.4204/eptcs.332.3
    issn: 2075-2180
  parent:
    type: periodical
    title: Electronic Proceedings in Theoretical Computer Science
    publisher: Open Publishing Association
    volume: 332
Cited by (1)

LNL polycategories and doctrines of linear logic shulman-2023-lnl

We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, Freyd-categories, and skew multicategories, as well as ordinary cartesian, symmetric, and planar multicategories and monoidal categories, symmetric polycategories, and linearly distributive and *-autonomous categories. To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine. We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.
DOI · arXiv
Cites 42 works (4 here)
With notes (4)

Proof Theory of Partially Normal Skew Monoidal Categories uustalu-2021-proof

DOI · arXiv

Eilenberg-Kelly Reloaded uustalu-2020-eilenberg

DOI

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

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-a

DOI · arXiv
External (38)
uustalu-2021-deductive reference entries/refs/uustalu-2021-deductive/uustalu-2021-deductive.hel