Stabilized profunctors and stable species of structures
Marcelo Fiore, Zeinab Galal, Hugo Paquet
TL;DR
The paper introduces stabilized profunctors built from groupoids equipped with Boolean kits, providing a two-dimensional refinement of Fiore–Gambino–Hyland–Winskel style generalized species. It demonstrates that this intensional framework yields a *-autonomous, cartesian closed bicategory SProf, with a linear exponential structure oc whose coKleisli yields stable species SEsp, and whose extensional counterpart is stable presheaves on Boolean kits. By constraining groupoid actions via kits, finitary polynomial functors on sets emerge as a special case, while the full extensional theory recovers analytic/polynomial functors between presheaf categories. The work develops a robust stable domain theory in a 2-categorical setting, including generic factorizations, local right adjoints, and cartesian natural transformations, and establishes a biequivalence between stable species and stable functors, thereby linking intensional stabilization with extensional presheaf semantics. Overall, the framework provides a new, rigorous model for classical linear logic and a refined lattice of functorial constructions between groupoid-based structures with potential applications to higher-order polynomial functors and differential linear logic.
Abstract
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.