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多范畴,该结构抽象了带有指数算子的经典线性逻辑的判据结构。现有许多结构均可表示为LNL多范畴,包括LNL伴随对、线性指数余单子、LNL多范畴、IL索引范畴、带存储的线性分配范畴、交换与强单子、CBPV结构、极化演算模型、Freyd范畴、斜多范畴,以及普通笛卡尔、对称、平面多范畴与幺半范畴、对称多范畴、线性分配范畴和*-自主范畴。为统一研究这些结构类,我们定义了LNL法则的概念,使得每一类结构均可被识别为某类法则的代数。我们证明LNL法则的自由代数可通过相继式演算呈现,且法则间的每个态射都会诱导其代数2-范畴之间的伴随对。