We introduce a bicategorical model of linear logic which is a novel variation of the bicategory of groupoids, profunctors, and natural transformations. Our model is obtained by endowing groupoids with additional structure, called a kit, to stabilize the profunctors by controlling the freeness of the groupoid action on profunctor elements. The theory of generalized species of structures, based on profunctors, is refined to a new theory of \emph{stable species} of structures between groupoids with Boolean kits. Generalized species are in correspondence with analytic functors between presheaf categories; in our refined model, stable species are shown to be in correspondence with restrictions of analytic functors, which we characterize as being stable, to full subcategories of stabilized presheaves. Our motivating example is the class of finitary polynomial functors between categories of indexed sets, also known as normal functors, that arises from kits enforcing free actions. We show that the bicategory of groupoids with Boolean kits, stable species, and natural transformations is cartesian closed. This makes essential use of the logical structure of Boolean kits and explains the well-known failure of cartesian closure for the bicategory of finitary polynomial functors between categories of set-indexed families and cartesian natural transformations. The paper additionally develops the model of classical linear logic underlying the cartesian closed structure and clarifies the connection to stable domain theory.

翻译：我们引入了一个线性逻辑的双范畴模型，它是群胚、预层函子和自然变换双范畴的一个新变体。该模型通过为群胚附加一种称为“工具包”（kit）的额外结构来实现，通过控制群胚在预层函子元素上作用的自由性来稳定预层函子。基于预层函子的广义结构种类理论被精炼为一个新理论，即具有布尔工具包的群胚之间的**结构稳定种类**。广义种类对应预层范畴之间的解析函子；在我们的精炼模型中，稳定种类被证明对应于解析函子在稳定预层完全子范畴上的限制，我们将此类限制刻画为“稳定的”。我们的激励示例是索引集范畴之间的有限多项式函子类（也称为正规函子），它由强制自由作用的工具包导出。我们证明了具有布尔工具包的群胚、稳定种类和自然变换组成的双范畴是笛卡尔闭的。这本质地利用了布尔工具包的逻辑结构，并解释了集合索引族范畴之间的有限多项式函子与笛卡尔自然变换双范畴笛卡尔闭性失效的著名现象。本文还发展了作为笛卡尔闭结构基础的经典线性逻辑模型，并阐明了与稳定域理论之间的联系。