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.
翻译:我们定义和研究了LNL poly范畴,这些范畴抽象了具有指数的经典线性逻辑的判断结构。许多现有的结构都可以表示为LNL poly范畴,包括LNL adjunctions、线性指数共单子、LNL multicategories、IL-indexed categories、具有存储的线性分配范畴、交换和强单子、CBPV-structures、极化演算模型、Freyd范畴和斜向多类,以及普通的笛卡尔、对称和平面多类和单子类、对称 poly范畴、线型分配和*-自主范畴。为了统一研究这些类别的结构,我们定义了LNL原理的概念,这样这些结构的每个类别都可以被识别为某种如此的原理的代数。我们表明,LNL原理的自由代数可以通过一个序列演算来呈现,每个原理的形态都会导致其2个类别之间的邻接。