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.

翻译：我们引入了一种线性逻辑的双范畴模型，该模型是对群胚、预层和自然变换之双范畴的全新变体。该模型通过赋予群胚额外结构（称为"工具包"）来实现，通过控制群胚对预层元素作用的自由性来稳定化预层。基于预层的广义结构种理论被精炼为一种新的理论——带布尔工具包的群胚之间的"稳定结构种"。广义结构对应预层范畴间的解析函子；在我们的精炼模型中，稳定结构被证明对应于解析函子（我们将其刻画为稳定的）到稳定化预层的全子范畴的限制。我们的激励例子是指数集范畴之间的有限多项式函子类（亦称正规函子），其源于强制自由作用的工具包。我们证明，带布尔工具包的群胚、稳定结构和自然变换构成的双范畴是笛卡尔闭的。这本质利用了布尔工具包的逻辑结构，并解释了已知事实：集合指数族范畴间的有限多项式函子与笛卡尔自然变换构成的双范畴为何缺乏笛卡尔闭性。本文进一步发展了支撑笛卡尔闭结构的经典线性逻辑模型，并阐明了其与稳定域理论的关联。