You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Mike Shulman (Jun 30 2021 at 00:50):I've posted a new preprint on the arXiv called LNL polycategories and doctrines of linear logic. Here's the abstract:
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, skew multicategories, as well as ordinary cartesian and symmetric multicategories and monoidal categories, 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.
One of my goals with this paper is to fill in some of the "missing foundation" for the not-yet-existent chapter 3 of my categorical logic notes. Another is to set up the definitions needed for a conjectural extension of *-autonomous envelopes and 2-conservativity of duals to theories with exponential modalities. Along the way I was surprised to find how many special cases of LNL polycategories have already been studied in the literature under different names with different technologies.
Mike Shulman (Jun 30 2021 at 05:00):I suppose possibly the middle of LICS was not the best time to post this preprint, but I couldn't wait any longer to get it off my to-do list. (-: It'll still be there next week. (Or next month.)
Nathanael Arkor (Jun 30 2021 at 11:47):The continual stream of examples of structures in the literature that are special cases of LNL polycategories is highly satisfying! The entries-only presentation is a neat solution to the combinatorics problem too. I need to come back and revisit the sections on doctrines (especially the connection between the SOA and inductive definitions, which sounds intriguing), but what I've read so far is very clear and compelling.
Chad Nester (Jul 02 2021 at 11:57):This looks very interesting! I wonder if it's possible to give proof nets for LNL polycategories.
Mike Shulman (Jul 02 2021 at 13:59):Surely!