Reference. Deductive Systems and Coherence for Skew Prounital Closed Categories
Cite
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.
Cites 42 works (4 here)
With notes (4)
Proof Theory of Partially Normal Skew Monoidal Categories uustalu-2021-proof
Eilenberg-Kelly Reloaded uustalu-2020-eilenberg
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 .
A theory of linear typings as flows on 3-valent graphs zeilberger-2018-a
External (38)
- Skew monoidal categories and skew multicategories (2018)
- The Sequent Calculus of Skew Monoidal Categories (2018)
- Monads need not be endofunctors (2015)
- Skew structures in 2-category theory and homotopy theory (2015)
- Linear logic without units (2013)
- Skew-closed categories (2012)
- Skew-monoidal categories and bialgebroids (2012)
- Skew monoidales, skew warpings and quantum categories (2012)
- Closed categories vs. closed multicategories (2012)
- Hereditary substitutions for simple types, formalized (2010)
- Closed categories (nLab) (2009)
- Temperley-Lieb algebra: from knot theory to logic and computation (2008)
- A Concurrent Logical Framework: The Propositional Fragment (2004)
- Categorical reconstruction of a reduction free normalization proof (1995)
- Natural deduction for intuitionistic linear logic (1995)
- Linear λ-calculus and categorical models revisited (1993)
- Logic Programming with Focusing Proofs in Linear Logic (1992)
- An inverse of the evaluation functional for typed lambda-calculus (1991)
- Non‐commutative intuitionistic linear logic (1990)
- Closed categories and the theory of proofs (1981)
- Algebra of Proofs (1978)
- Coherence in nonmonoidal closed categories (1977)
- The Connection between Equivalence of Proofs and Cartesian Closed Categories (1975)
- Symmetric closed categories (1975)
- A categorical equivalence of proofs (1974)
- The correspondence between cut-elimination and normalization (1974)
- Deductive systems and categories III. Cartesian closed categories, intuitionist propositional calculus, and combinatory logic (1972)
- Coherence in closed categories (1971)
- Erratum (1971)
- Equality in hyperdoctrines and comprehension schema as an adjoint functor (1970)
- Deductive systems and categories II. Standard constructions and closed categories (1969)
- Deductive systems and categories I: Syntactic calculus and residuated categories (1968)
- Closed Categories (1966)
- Natural Deduction: A Proof-Theoretical Study (1965)
- On MacLane's conditions for coherence of natural associativities, commutativities, etc (1964)
- Notes on the axiomatics of the propositional calculus (1963)
- Catégories avec multiplication (1963)
- Natural associativity and commutativity (1963)