We introduce a new bicategorical model of linear logic based on profunctors between groupoids. This model is a new variation of the usual bicategory of profunctors, obtained by endowing groupoids with additional structure to constrain the profunctors. One goal of this new model is to provide a formal bridge between the model of finitary polynomial functors, also known as normal functors, and the combinatorial theory of generalized species of structures. Our approach consists in viewing finitary polynomial functors as analytic functors generated by free generalized species. The main conceptual novelty is the notion of kit, designed to control the extent to which species are free. We study kits from both combinatorial and logical perspectives. Profunctors that respect the kit structure are called stabilized, and the bicategory of stabilized profunctors gives rise to stable species of structures, a cartesian closed bicategory that embeds finitary polynomial functors. Stabilized profunctors and stable species can be given an extensional presentation as certain functors between subcategories of presheaves determined by the kit. This gives a strict 2-categorical presentation of the same model.
翻译:我们引入了一种基于群胚间共轭函子的线性逻辑双范畴新模型。该模型是通常共轭函子双范畴的一个新变体,通过赋予群胚额外结构来约束共轭函子而得。此新模型的目标之一是为有限多项式函子(亦称正规函子)模型与广义结构物种组合理论之间建立形式桥梁。我们的方法将有限多项式函子视为由自由广义物种生成的分析函子。主要概念创新在于"工具包"(kit)这一概念,旨在控制物种自由程度的范围。我们从组合与逻辑双重角度研究了工具包。尊重工具包结构的共轭函子被称为稳定化共轭函子,而稳定化共轭函子双范畴衍生出结构稳定物种,这是一个嵌入有限多项式函子的笛卡尔闭双范畴。稳定化共轭函子与稳定物种可通过工具包决定的预层子范畴间的特定函子获得外延表示,从而为同一模型提供了严格2-范畴化表述。