一句话：通过给 groupoid 加 kit 来稳定 profunctor，建立线性逻辑的双范畴模型，并证明稳定 species 双范畴笛卡尔闭。
论文为线性逻辑提出一种新的双范畴模型，改造由 groupoid、profunctor 与自然变换构成的双范畴。方法是在 groupoid 上附加 kit 结构，控制作用在 profunctor 元素上的自由性以稳定 profunctor，从而将广义 species of structures 理论细化为 Boolean kit 间的稳定 species 理论。文章证明稳定 species 对应稳定化 presheaf 满子范畴上解析函子的限制，并联系稳定域理论。作为动机例子，索引集合范畴间的 finitary polynomial functor（normal functor）可由 kit 强制自由作用得到。关键结果是该双范畴是笛卡尔闭的，解释了 finitary polynomial functor 双范畴笛卡尔闭性的失败。
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.
@article{paperbot2774,
title = {Stabilized profunctors and stable species of structures},
author = {Marcelo Fiore and Zeinab Galal and Hugo Paquet},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:17)2024}
}