A practical type theory for symmetric monoidal categories

zbMath1474.18031arXiv1911.00818MaRDI QIDQ5006460

Michael Shulman

Publication date: 16 August 2021

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

zbMATH Keywords

coalgebratype theorysymmetric monoidal categoryprop

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Monoidal categories, symmetric monoidal categories (18M05) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45) Polycategories/dioperads, properads, PROPs, cyclic operads, modular operads (18M85)

Related Items (2)

Coherence via focusing for symmetric skew monoidal categories ⋮ The syntactic side of autonomous categories enriched over generalised metric spaces

Uses Software

• MathOverflow

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Traces in symmetric monoidal categories
• Weakly distributive categories
• Weak Hopf monoids in braided monoidal categories.
• Natural deduction and coherence for weakly distributive categories
• Coherence for compact closed categories
• The geometry of tensor calculus. I
• A Survey of Graphical Languages for Monoidal Categories
• A formal language for cyclic operads
• *-Autonomous categories and linear logic
• Polycategories
• Props in Network Theory
• Traced monoidal categories
• Abstract Tensor Systems as Monoidal Categories
• Categorical algebra
• Linear logic propositions as session types

This page was built for publication: A practical type theory for symmetric monoidal categories