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)”的额外结构来获得，通过控制群胚对预函子元素作用的自由性，从而实现预函子的稳定化。基于预函子的广义结构物种理论被精炼为一类新的理论，即具有布尔工具箱的群胚之间的*稳定物种*。广义结构与预层范畴之间的解析函子相对应；在我们的精炼模型中，稳定结构被证明与解析函子的限制相对应，我们将其刻画为对稳定化预层全子范畴的稳定解析函子。我们的动机范例是索引集范畴之间的有限多项式函子类（也称为正规函子），它源于强化自由作用的工具箱。我们证明，具有布尔工具箱的群胚、稳定物种和自然变换构成的双范畴是笛卡尔封闭的。这本质地使用了布尔工具箱的逻辑结构，并解释了众所周知的关于集合索引族范畴之间的有限多项式函子与笛卡尔自然变换构成的双范畴缺乏笛卡尔封闭性的原因。本文还进一步发展了支撑笛卡尔封闭结构的经典线性逻辑模型，并阐明了其与稳定域理论的联系。