LNL polycategories and doctrines of linear logic

TL;DR

This paper introduces LNL polycategories and doctrines to unify various categorical structures in linear logic, providing a framework for their analysis and construction via algebraic and sequent calculus methods.

Contribution

It defines LNL polycategories and doctrines, unifying many existing structures in linear logic and categorical semantics under a common framework.

Findings

LNL polycategories encompass numerous known structures in linear logic.

A sequent calculus for free algebras of LNL doctrines is developed.

Morphisms of doctrines induce adjunctions between algebra categories.

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, 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.