# STABILIZED PROFUNCTORS AND STABLE SPECIES OF STRUCTURES

MARCELO FIORE ◦ª, ZEINAB GALAL ◦ᵇ, AND HUGO PAQUET ◦ᶜ

ª University of Cambridge
*e-mail address:* marcelo.fiore@cl.cam.ac.uk

ᵇ Sorbonne University
*e-mail address:* zeinab.galal@lip6.fr

ᶜ University of Oxford
*e-mail address:* hugo.paquet@cs.ox.ac.uk

**ABSTRACT.** We define a new bicategorical model of linear logic that refines the bicategory of groupoids, profunctors, and natural transformations. An object of this new model is a groupoid with additional structure, called a *Boolean kit*, used to constrain profunctors by stabilizing the groupoid action on their elements.

The theory of generalized species of structures, based on profunctors, is then refined to a new theory of *stable species* of structures between groupoids with Boolean kits. While generalized species are in correspondence with analytic functors between presheaf categories, stable species are shown to correspond to *stable functors* between full subcategories of presheaves determined by the kits. One motivation for stable functors is that, in the special case where kits enforce free actions, they correspond to finitary polynomial functors between categories of indexed sets, also known as normal functors.

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 indexed sets) 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.

*Key words and phrases:* Categorical models, Polynomial functors, Bicategories, Species of structures, Linear logic, Denotational semantics.

The first author was partially supported by the EPSRC grant EP/V002309/1. The second author was supported by the PPS ANR project (ANR-19-CE48-0014), the EPSRC grant EP/V002309/1, and the PGRM Emergence project. The third author was supported by a Royal Society University Research Fellowship, and a Marie Skłodowska-Curie grant co-funded by the Paris Region and the EU under Horizon 2020.
# 1. INTRODUCTION

Profunctors, sometimes called distributors or bimodules, are categorical structures appearing in various areas of logic and computer science. This paper is concerned with profunctors between *groupoids* and their application to linear logic and structural combinatorics. A main goal is to develop a formal connection with the theory of *polynomial functors* [Koc12, AAG05]. Let us summarize the context and the main results of the paper.

**Profunctors in logic and combinatorics.** A profunctor from $\mathbb{A}$ to $\mathbb{B}$, where $\mathbb{A}$ and $\mathbb{B}$ are categories, is a functor $\mathbb{B}^{\circ} \times \mathbb{A} \to \mathbf{Set}$ [Yon60, Bén67, Bén00, Law73]. It is common to define a bicategory whose objects are small categories, morphisms are profunctors, and 2-cells are natural transformations; in this paper we will call **Prof** the full sub-bicategory whose objects are *groupoids*.

The bicategory **Prof** has well-known logical and combinatorial features [Tay89, FGHW08] that we briefly summarize now; more details are given in Section 3.1. First, **Prof** is a model of linear logic [Gir87]: the various logical connectives are defined with sums, products, or opposites of groupoids, and the exponential modality $\Sigma\mathbb{A}$ is constructed by considering symmetric sequences of objects of $\mathbb{A}$. We can then explain the combinatorial nature of **Prof** in this language: if **1** is the trivial one-object groupoid, then profunctors in **Prof(\Sigma1, 1)** correspond to combinatorial *species of structures* in the sense introduced by Joyal [Joy81]. The coKleisli bicategory **Prof<sub>Σ</sub>** is known as the bicategory of *generalized species of structures* [FGHW08], since one can consider combinatorial species between groupoids other than **1**.

The bicategory **Prof<sub>Σ</sub>** is cartesian closed [FGHW08] and forms the basis for a number of models for typed and untyped $\lambda$-calculus. These models can be used, for instance, to track the symmetries of resource usage [Oli21] or the combinatorics of reduction paths [TAO17, TAO18].

**Polynomial functors and analytic functors.** The starting point for this paper is a connection between Joyal's combinatorial species and polynomial functors on sets, that we review briefly (Section 2 contains full details).

On one side, we consider *finitary* polynomial functors **Set** $\to$ **Set**, which correspond to operators on sets of the form

$$X \mapsto \sum_{n \in \mathbb{N}} A_n \times X^n \qquad (1.1)$$

where the coefficients $A_n$ are sets. On the other side, a combinatorial species consists of a family of sets $F_n$, for $n \in \mathbb{N}$, equipped with a left action of the symmetric group $\mathfrak{S}_n$ on $n$ elements. This determines a functor **Set** $\to$ **Set** of the form

$$X \mapsto \sum_{n \in \mathbb{N}} F_n \times_{\mathfrak{S}_n} X^n \qquad (1.2)$$

where the operator $\mathfrak{S}_n^\times$ performs a quotient of the product under the action. A functor of this form is known as an *analytic functor*, and every analytic functor has a unique generating species, up to isomorphism [Joy86].

In special cases, when the actions on $F_n$ are *free actions* (§2.3), the quotient is equivalently a set of the form $A_n \times X^n$, and so the analytic functor is also polynomial. Conversely, every
finitary polynomial functor is analytic when its coefficients are regarded as freely generated actions.

Thus, finitary polynomial functors determine a subcategory of $\mathbf{Prof}(\Sigma 1, 1)$, and the language of species gives a basic combinatorial perspective on polynomial functors. Our purpose here is to generalize this connection, and to provide a new *logical* perspective, following the methodology offered by the logical structure of profunctors and generalized species.

**Contributions of this paper.** We extend the correspondence between finitary polynomial functors and free analytic functors to a wider setting: instead of functors over the category of sets, we consider functors between full subcategories of presheaves over groupoids. Our first contribution is a logical device for constraining the actions on the coefficients of analytic functors: in particular one may require all actions to be free. We call this device a *kit* (Section 4.1).

In Section 4.2, we define a refinement of **Prof** called **SProf**, in which groupoids are equipped with kits in order to constrain the profunctors between them. Profunctors that respect the kit structure are called *stabilized*. The bicategory **SProf** has the following key properties: it is a model of linear logic, and the logical structure is preserved by the forgetful functor **SProf** → **Prof** (Section 5). The category **SProf**($\Sigma 1, 1$) is the sub-category of **Prof**($\Sigma 1, 1$) that corresponds to finitary polynomial functors on sets.

Thus, we can use the logical structure of **SProf** as a new language for polynomial functors operating on groupoid actions. We recover well-known notions of polynomial functors operating on sets [Gir88, AGH$^+$15] and we obtain a new notion of polynomial functors of higher-order<fnref n="1" /> type.

For example, the kits can be used to characterize, among the profunctors in $\mathbf{Prof}(\Sigma 1, 1)$, those corresponding to polynomial functors on sets. We focus on this special case in Section 2, and give the general theory in Section 4.1. Kits are largely inspired by the *creeds* of Taylor [Tay89], although we have crucially taken a different approach based on double orthogonality. As explained in Section 5.2, this allows us to model the involutive negation of classical linear logic.

**Intensional and extensional perspectives.** One important aspect of this paper is the dichotomy between *intensional* and *extensional* presentations. This is a recurrent theme in the semantics of linear logic and in the theory of species, as illustrated by the table of examples in Figure 1. Our model of stabilized profunctors between groupoids with kits can also be presented in extensional form. We show that a kit $\mathcal{A}$ on a groupoid $\mathcal{A}$ determines a full subcategory $\mathcal{S}(\mathcal{A}, \mathcal{A})$ of the presheaf category $\mathcal{P}(\mathcal{A})$, and that a stabilized profunctor $P \in \mathbf{SProf}((\mathcal{A}, \mathcal{A}), (\mathcal{B}, \mathcal{B}))$ is equivalently given by a *linear* functor $\mathcal{S}(\mathcal{A}, \mathcal{A}) \to \mathcal{S}(\mathcal{B}, \mathcal{B})$, where *linear* means that the functor preserves filtered colimits, and has a left and a right adjoint on every slice (Definition 9.1).

From the combinatorial perspective, it is the coKleisli bicategory $\mathbf{SProf}_\Sigma$ for the exponential comonad which is of primary interest, because of the connection to generalized species. We show that the morphisms in that bicategory can be presented extensionally as *stable* functors $\mathcal{S}(\mathcal{A}, \mathcal{A}) \to \mathcal{S}(\mathcal{B}, \mathcal{B})$, where stability relaxes linearity by not requiring a right

<footnote n="1">¹Note that this ‘higher-order’ structure refers to a bicategory whose *morphisms* are polynomial functors. Polynomial functors over **Set** are also the *objects* of a category which is known to be cartesian closed [ALS10].</footnote>
<table><caption>Figure 1: Well-known categorical structures in extensional and intensional form. In the table, A and B are groupoids and M<sub>fin</sub> is the finite multiset construction.</caption><thead><tr><th></th><th>EXTENSIONAL PRESENTATION</th><th>INTENSIONAL PRESENTATION</th></tr></thead><tbody><tr><td>Scott [Sco76]</td><td>Continuous functions</td><td>Finitary graphs of continuous functions</td></tr><tr><td>Girard [Gir88]</td><td>Normal functors<br>Set<sup>I</sup> → Set</td><td>Power series coefficients<br>M<sub>fin</sub>(I) → Set</td></tr><tr><td>Gambino, Kock [GK13]</td><td>Polynomial functors<br>Set/I → Set/J</td><td>Polynomial diagrams<br>I ← E → B → J</td></tr><tr><td>Joyal [Joy81]</td><td>Analytic functors<br>Set → Set</td><td>Species of structures<br>Bij → Set</td></tr><tr><td>Morita, Watts<br>Lawvere, Bénabou</td><td>Colimit-preserving functors<br>P(A) → P(B)</td><td>Profunctors<br>B<sup>°</sup> × A → Set</td></tr><tr><td>Fiore et al. [Fio14, FGHW08]</td><td>Analytic functors<br>P(A) → P(B)</td><td>Generalized species<br>B<sup>°</sup> × ΣA → Set</td></tr></tbody></table>

adjoint on each slice and requiring the preservation of epimorphisms (Definition 8.4). This terminology comes from stable domain theory [Ber78, Tay90, Lam88], as we discuss further in Section 8.

The conference version of this paper focused on the bicategory **SEsp** = **SProf**<sub>Σ</sub>, described directly, and on the correspondence with stable functors [FGP22]. This longer version provides all details, including the underlying linear theory of stabilized profunctors.

**Structure of the paper.** Beyond the two background sections that follow, the paper is organized into two main parts. In the first part (Sections 4 to 6), we regard profunctors as groupoids actions, and introduce kits to control and stabilize these actions. We study kits from a logical perspective, and introduce an orthogonality relation for families of subgroups of endomorphisms in a groupoid. The induced Boolean algebra structure gives rise to the notion of Boolean kit. We show that the bicategory of Boolean kits and stabilized profunctors is a model of differential linear logic.

In the second part (Sections 7 to 9), we study the extensional aspects of stabilized profunctors and stable species. We show that orthogonality for kits can be translated to an orthogonality relation on presheaves. We then prove that stabilized profunctors and stable species can be characterized respectively as linear and stable functors between subcategories of presheaves closed under double-orthogonality. This provides a 2-dimensional stable domain theory.
## 2. MOTIVATION: POLYNOMIAL AND ANALYTIC FUNCTORS OVER SETS

At the heart of this paper is the relationship between two families of functors from **Set** to **Set**: finitary polynomial functors (also known as normal functors) and analytic functors. We start by giving the relevant definitions.

**Polynomial functors.** A function $p : E \to B$ between sets $E$ and $B$ determines an endofunctor on **Set** defined as

$$X \mapsto \sum_{b \in B} X^{E_b}$$

where $E_b = p^{-1}\{b\}$ is the fibre of $p$ over $b \in B$, and $X^{E_b}$ is the set of functions $E_b \to X$. A functor of this form is called a polynomial functor. If we restrict to those $p$ such that $E_b$ are finite sets for all $b \in B$, then the functor is naturally isomorphic to one of the form

$$X \mapsto \sum_{n \in \mathbb{N}} F_n \times X^n \qquad (2.1)$$

where each set $F_n$ corresponds to the set of all $b \in B$ such that $|E_b| = n$. The analogy with traditional polynomials is manifest in this representation. These polynomial functors are called *finitary* and are determined by their action on finite input sets.

**Analytic functors.** We now turn to a strictly more general family of functors. An endofunctor on **Set** is an *analytic functor* [Joy86] if it is naturally isomorphic to one of the form

$$X \mapsto \sum_{n \in \mathbb{N}} F(n) \times X^n, \qquad (2.2)$$

where:

(1) Each $F(n)$ is a set with a left action of the symmetric group $S_n$ on $n$ elements. Concretely, this means that we have an assignment that to every permutation $\sigma \in S_n$ of the set $[n] = \{1, \dots, n\}$ associates a permutation of the set $F(n)$ preserving identity and composition. We write $\sigma \cdot p$ for the action of $\sigma \in S_n$ on an element $p \in F(n)$.

(2) The set $F(n) \times X^n$ is obtained by quotienting the product $F(n) \times X^n$ under the equivalence relation $\sim$ containing the pairs

$$(p, (x_{\sigma 1}, \dots, x_{\sigma n})) \sim (\sigma \cdot p, (x_1, \dots, x_n))$$

for all $\sigma \in S_n$, $p \in F(n)$ and $(x_1, \dots, x_n) \in X^n$.

The notation $F(-)$ is justified, because the coefficients $F(n)$, together with the group actions, can be bundled into a functor $F: \mathbf{Bij} \to \mathbf{Set}$ where **Bij** is the category whose objects are the natural numbers, and whose morphisms $m \to n$ are the bijections $[m] \to [n]$. This category is equivalent to the category of finite sets and bijections. The action of a permutation $\sigma \in S_n$ on the set $F(n)$ is then simply given by the functorial action $F(\sigma) : F(n) \to F(n)$.

The functor $F: \mathbf{Bij} \to \mathbf{Set}$ is a species of structures (or just a species, with its elements referred to as structures) corresponding to the analytic functor (2.2). Every analytic functor has, up to isomorphism, a unique generating species, which may be recovered using so-called weak generic elements (Section 8.1).

For some more combinatorial intuition, each $F(n)$ is intended to model a type of structures (trees, partitions, ...) with $n$ labels (indexed 1 to $n$) on which the symmetric group acts by permutation. The induced analytic functor then constructs for each set $X$
the set of X-labelled F-structures. These are elements of $F(n)$ at any $n$ in which labels are elements of X. This theory was developed by Joyal [Joy81, Joy86] for application in combinatorics. Joyal also noticed the connection to polynomial functors that we explain next.

**Finitary polynomial functors are free analytic functors.** Finitary polynomial functors can be identified with the sub-family of free analytic functors. The basic idea is as follows. Every set $A$ generates a free action of a group $G$, given by the product set $A \times G$ with the action

$$ \tau \cdot (a, \sigma) := (a, \tau \sigma) \qquad (2.3) $$

for every $\tau \in G$ and $(a, \sigma) \in A \times G$. We extend this to polynomial functors. Consider the finitart polynomial functor $X \mapsto \sum_{n \in \mathbb{N}} A_n \times X^n$. Taking the free action generated by $A_n$ of $\mathfrak{S}_n$, for every $n \in \mathbb{N}$, we obtain a species **Bij** $\to$ **Set** given by

$$ n \mapsto A_n \times \mathfrak{S}_n \\ (\tau : n \to n) \mapsto ((a, \sigma) \mapsto (a, \tau \sigma)) $$

which, via the construction (2.2), generates an analytic functor. For this species, when taking the quotient in (2.2), we have

$$ (A_n \times \mathfrak{S}_n) \times_{\mathfrak{S}_n} X^n \cong A_n \times X^n $$

and therefore recover the polynomial functor. Thus, every finitary polynomial functor is, in particular, analytic.

**Stabilizer subgroups and free species.** In this paper, “finitary polynomial” and “analytic” are viewed as the two extremes in a spectrum of classes of functors **Set** $\to$ **Set**. The intermediate classes are defined in terms of the underlying species of structures, using a new notion we call a kit.

Recall that, if a group $G$ acts on a set $P$, the stabilizer of an element $p \in P$, defined as $\text{Stab}_G(p) := \{\sigma \in G \mid \sigma \cdot p = p\}$, is a subgroup of $G$. The key observation is that free actions, as in (2.3), are exactly those for which every element has trivial stabilizer. Thus, if $F : \text{Bij} \to \text{Set}$ is a species such that for every $n \in \mathbb{N}$, the action of $\mathfrak{S}_n$ on $F(n)$ is free in the sense that every structure in $F(n)$ has trivial stabilizer, then the associated analytic endofunctor on **Set** is polynomial. This characterizes the analytic functors that are polynomial in terms of their generating species.

**Kits on Bij.** One key idea of this paper is to use families of subgroups to specify the extent to which a species may be free. Indeed, by specifying, for each $n \in \text{Bij}$, a set $\mathcal{K}(n)$ of subgroups of $\text{Bij}(n, n)$ that are to be regarded as permitted stabilizers, we may restrict to species with structures having only permitted stabilizers and thereby identify a class of functors **Set** $\to$ **Set**.

As extreme special cases, one can take $\mathcal{K}(n)$ to contain all the subgroups of $\text{Bij}(n, n)$ and recover the analytic functors; or, instead, take $\mathcal{K}(n)$ to consist only of the trivial subgroup, forcing the species to be free, and recover polynomial functors. Such families of subgroups $\mathcal{K} = \{\mathcal{K}(n)\}_{n \in \text{Bij}}$, subject to a compatibility condition, will be called kits (Definition 4.1).

There is no need that the choice of permitted stabilizers be uniform across all $n \in \text{Bij}$ as in the two examples above. But it is natural to require that permitted stabilizers are closed
under conjugation, since for every structure $p \in F(n)$ and permutation $\sigma \in \mathbf{Bij}(n, n)$, the stabilizer subgroups of $p$ and of $\sigma \cdot p$ are conjugate of each other: $\mathrm{Stab}(\sigma \cdot p) = \sigma \mathrm{Stab}(p) \sigma^{-1}$.

First we appropriately restrict species:

**Definition 2.1.** For each $n \in \mathbf{Bij}$, let $\mathcal{K}(n)$ be a family of subgroups of $\mathbf{Bij}(n, n)$ closed under conjugation, and write $\mathcal{K} = \{\mathcal{K}(n)\}_{n \in \mathbf{Bij}}$. A $\mathcal{K}$-species is a functor $F : \mathbf{Bij} \to \mathbf{Set}$ such that every element of $F(n)$ has stabilizer in $\mathcal{K}(n)$.

This way, every family $\mathcal{K}$ determines a subclass of analytic endofunctors on $\mathbf{Set}$, namely, those whose generating species are $\mathcal{K}$-species. We will call such a family a kit on the groupoid **Bij**.

By varying the kit structure, one obtains different subclasses of analytic functors on $\mathbf{Set}$. This paper is primarily about the connection to polynomial functors, so our construction of stable species in terms of a linear exponential comonad (Section 6) corresponds to the kit on **Bij** that consists of only the trivial subgroups. On the other hand, Joyal's species are arbitrary functors and correspond to the maximal kit containing all subgroups.

### 3. PRELIMINARIES ON PROFUNCTORS AND GENERALIZED SPECIES

This paper extends the connection between polynomial functors and analytic functors to a generalized setting based on profunctors. In this section, we recall some important background: we describe the construction of a bicategory of profunctors (e.g. [Yon60, Bén67, Bén00, Law73]) and of the induced bicategory of generalized species.

**3.1. Profunctors.** For groupoids $\mathcal{A}$ and $\mathcal{B}$, a profunctor $P : \mathcal{A} \dashrightarrow \mathcal{B}$ is a functor $\mathcal{B}^{\circ} \times \mathcal{A} \to \mathbf{Set}$. This is a family of sets indexed by pairs of objects $a \in \mathcal{A}$ and $b \in \mathcal{B}$, and with an action of the two groupoids. We use the following notation: if $(b, a) \in \mathcal{B}^{\circ} \times \mathcal{A}$, $p \in P(b, a)$, $\alpha \in \mathcal{A}(a, a')$ and $\beta \in \mathcal{B}(b', b)$, we write

$$ \alpha \cdot p := P(\mathrm{id}_b, \alpha)(p) \in P(b, a') $$

$$ p \cdot \beta := P(\beta, \mathrm{id}_a)(p) \in P(b', a) $$

and by functoriality, the two actions commute.

A profunctor $\mathcal{A} \dashrightarrow \mathcal{B}$ is equivalently a functor $P : \mathcal{A} \to \mathcal{P}(\mathcal{B})$, and it is helpful to think of this as a Kleisli arrow for the presheaf construction $\mathcal{P}$ (cf. [FGHW18]). Since $\mathcal{A}$ is a dense subcategory of $\mathcal{P}(\mathcal{A})$, we can define a functor $\mathcal{P}(\mathcal{A}) \to \mathcal{P}(\mathcal{B})$ as the unique colimit-preserving functor that extends $P$. Formally this is a left Kan extension, as we use next.

*The bicategory of profunctors over groupoids.* Two profunctors $P : \mathcal{A} \dashrightarrow \mathcal{B}$ and $Q : \mathcal{B} \dashrightarrow \mathcal{C}$ compose to give $Q \circ P : \mathcal{A} \dashrightarrow \mathcal{C}$, defined as the composite functor $(\mathrm{Lan}_{\mathcal{Y}_{\mathcal{B}}} Q) P$ where $\mathrm{Lan}_{\mathcal{Y}_{\mathcal{B}}} Q$ denotes the left Kan extension of $Q$ along the Yoneda embedding $\mathrm{y}_{\mathcal{B}} : \mathcal{B} \hookrightarrow \mathcal{P}\mathcal{B}$:

<figure><img src="image_1.png" /></figure>
There is a more concrete pointwise formula for $Q \circ P$ in terms of a coend:

$$ (Q \circ P)(c, a) := \int_{b \in \mathbb{B}} P(b, a) \times Q(c, b) \cong \left( \coprod_{b \in \mathbb{B}} P(b, a) \times Q(c, b) \right) / \sim $$

where $\sim$ is the least equivalence relation such that

$$ (b, p \cdot \beta, q) \sim (b', p, \beta \cdot q) $$

for $p \in P(b', a)$, $q \in Q(c, b)$ and $\beta : b \to b' \in \mathbb{B}$.

The identity profunctor is the hom-functor $\mathbb{A}^{\circ} \times \mathbb{A} \to \mathbf{Set}$, defined as $(a, a') \mapsto \mathbb{A}(a, a')$. The composition of profunctors is only associative and unital up to natural isomorphism, and thus we have the following bicategory:

**Definition 3.1.** We denote by **Prof** the bicategory given by:

* objects: small groupoids $\mathbb{A}, \mathbb{B}$;

* 1-cells: profunctors $P : \mathbb{A} \dashrightarrow \mathbb{B}$;

* 2-cells: natural transformations.

*Profunctors in extensional form.* As we mentioned, a profunctor $P : \mathbb{A} \dashrightarrow \mathbb{B}$ induces a unique colimit-preserving functor $\mathcal{P}(\mathbb{A}) \to \mathcal{P}(\mathbb{B})$ between the presheaf categories (Theorem 3.3). In this representation, the composition of profunctors reduces to a composition of functors, so we have a 2-category.

**Definition 3.2.** We denote by **Cocont** the 2-category given by:

* objects: small groupoids $\mathbb{A}, \mathbb{B}$;

* 1-cells: cocontinuous functors $F : \mathcal{P}\mathbb{A} \to \mathcal{P}\mathbb{B}$;

* 2-cells: natural transformations.

**Theorem 3.3.** *The bicategory Prof and the 2-category Cocont are biequivalent.*

## 3.2. Generalized species.
We now describe a bicategory of generalized species of structures indexed by arbitrary groupoids.

*From species to generalized species.* For a species of structures **Bij** $\to$ **Set**, consider the following two basic observations. First, the groupoid **Bij** is the free symmetric strict monoidal completion of the terminal category **1**. This completion is denoted $\Sigma\mathbf{1}$ and described formally below. Second, **Set** is isomorphic to the category of presheaves $\mathcal{P}\mathbf{1}$ over **1**. The version, due to Fiore, Gambino, Hyland and Winskel [FGHW08] extends the basic notion of a species **Bij** $\to$ **Set**, corresponding to $\Sigma\mathbf{1} \to \mathcal{P}\mathbf{1}$, to

$$ \Sigma\mathbb{A} \to \mathcal{P}\mathbb{B} \qquad (3.1) $$

for $\mathbb{A}$ and $\mathbb{B}$ groupoids (in fact, they can be arbitrary small categories, but we do not use this generality here). Their main result is that these assemble into a bicategory **Esp** of groupoids, generalized species, and natural transformations, and that moreover this bicategory is cartesian closed.

Since $\mathcal{P}(\mathbb{B}) = [\mathbb{B}^{\circ}, \mathbf{Set}]$, a generalized species is equivalently a profunctor $\mathbb{B}^{\circ} \times \Sigma\mathbb{A} \to \mathbf{Set}$, and the bicategory **Esp** can be obtained as a coKleisli bicategory for the pseudo-comonad $\Sigma$ over the bicategory of profunctors. This is the approach we follow in this paper.
**The symmetric strict monoidal completion.** For a category $\mathcal{A}$, define $\Sigma\mathcal{A}$ as the category whose objects are finite sequences $\langle a_1, \dots, a_n \rangle$ of objects of $\mathcal{A}$ and a morphism $\alpha$ between two sequences $\langle a_1, \dots, a_n \rangle$ and $\langle b_1, \dots, b_n \rangle$ consists of a pair $(\sigma, (\alpha_i)_{i \in [n]})$ where $\sigma$ is a permutation of the set $[n] = \{1, \dots, n\}$ and $(\alpha_i : a_i \to b_{\sigma(i)})_{i \in [n]}$ is a sequence of morphisms in $\mathcal{A}$. There are no morphisms in $\Sigma\mathcal{A}$ between sequences of different lengths.

If $\mathcal{A}$ is a groupoid, then $\Sigma\mathcal{A}$ is also a groupoid, equipped with a symmetric monoidal structure given by the concatenation of sequences $(u, v) \mapsto u \otimes v$. This construction has a canonical 2-monad structure on **Cat**, that can be lifted to a pseudo-comonad on **Prof**, see e.g. [FGHW18]. It maps a profunctor $P : \mathcal{A} \dashrightarrow \mathcal{B}$ to the profunctor $\Sigma P : \Sigma\mathcal{A} \dashrightarrow \Sigma\mathcal{B}$ given by:

$$ \Sigma P(\langle a_i \rangle_{i \in [n]}, \langle b_j \rangle_{j \in [m]}) = \begin{cases} \coprod_{\varphi \in \mathfrak{S}_n} \coprod_{j \in [m]} P(b_j, a_{\varphi(j)}), & \text{if } n = m \\ \emptyset, & \text{otherwise} \end{cases} $$

The counit and comultiplication, denoted der and dig respectively (for *dereliction* and *digging*, following the usual terminology of linear logic) are pseudo-natural transformations whose components are the profunctors

$$ \mathrm{der}_{\mathcal{A}} : \Sigma\mathcal{A} \dashrightarrow \mathcal{A} $$

$$ (a, u) \mapsto \Sigma\mathcal{A}(\langle a \rangle, u) $$

$$ \mathrm{dig}_{\mathcal{A}} : \Sigma\mathcal{A} \dashrightarrow \Sigma\Sigma\mathcal{A} $$

$$ (\langle u_1, \dots, u_n \rangle, u) \mapsto \Sigma\mathcal{A}(u_1 \otimes \dots \otimes u_n, u). $$

**The bicategory of species.** Generalized species of structures are the morphisms in the coKleisli bicategory **Prof**<sub>Σ</sub>, which we call **Esp**. In other words, **Esp**(*A*, **B**) consists of profunctors of the form $\Sigma\mathcal{A} \dashrightarrow \mathcal{B}$ and natural transformations between them; observe that the category **Esp**(1, 1) is the category of combinatorial species in the sense of Joyal.

Just as a species **Bij** $\to$ **Set** induces an analytic functor **Set** $\to$ **Set**, a generalized species $F : \Sigma\mathcal{A} \to \mathcal{P}(\mathcal{B})$ induces an analytic functor $\mathcal{P}(\mathcal{A}) \to \mathcal{P}(\mathcal{B})$ that transports a presheaf $X \in \mathcal{P}(\mathcal{A})$ to the presheaf

$$ b \mapsto \int^{\langle a_i \rangle \in \Sigma\mathcal{A}} F(b, \langle a_i \rangle) \times \mathcal{P}(\mathcal{A})\left(\coprod_{i=1}^{n} y(a_i), X\right) $$

for $b \in \mathcal{B}$. This formula, and indeed the earlier one for Joyal species (2.2), are obtained as left Kan extensions:

**Proposition 3.4.** For groupoids $\mathcal{A}, \mathcal{B}$, and a generalized species $F : \Sigma\mathcal{A} \dashrightarrow \mathcal{B}$, the analytic functor described pointwise above is a left Kan extension of $F$ along the functor $s : \Sigma\mathcal{A} \to \mathcal{P}(\mathcal{A}) : \langle a_1, \dots, a_n \rangle \mapsto \coprod_{i=1}^n y(a_i)$, as on the left below:

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

For $\mathcal{A} = \mathcal{B} = 1$ and $F$ viewed as a species **Bij** $\to$ **Set**, this corresponds to the diagram on the right above, where $j$ is the inclusion functor, and induces the formula (2.2).
We note that, for a species $F$ in $\mathbf{Esp}(\mathbb{A}, \mathbb{B})$ the induced analytic functor is the same, under the equivalence $\mathcal{P}(\mathbb{A}) \simeq \mathbf{Esp}(0, \mathbb{A})$ for $0$ the empty groupoid, as the post-composition functor

$$F \circ - : \mathbf{Esp}(0, \mathbb{A}) \to \mathbf{Esp}(0, \mathbb{B}).$$

Analytic functors between presheaf categories over groupoids can be characterized directly, thus giving an extensional presentation of $\mathbf{Esp}$ as a strict 2-category [Fio14]. We will not need this characterization in the paper, so we omit it.

# INTENSIONAL THEORY: STABILIZED PROFUNCTORS AND STABLE SPECIES

We proceed to develop our new model based on groupoids with kits. We first study profunctors and species over groupoids with kits; this is what we call the “intensional theory”. This provides a refinement of the bicategories **Prof** and **Esp**.

## 4. KITS AND STABILIZED PROFUNCTORS

### 4.1. Groupoids and Kits.
We first make some basic remarks about groupoids, and fix some notation. For every object $a$ in a groupoid $\mathbb{A}$, the set of endomorphisms $\mathrm{End}_{\mathbb{A}}(a) = \mathbb{A}(a, a)$ forms a group under composition. The groups $\mathrm{End}_{\mathbb{A}}(a)$ will play a central role in our development and we often simply write $\mathrm{End}(a)$.

For a group $G$, we write $H \leq G$ to mean that $H$ is a subgroup of $G$; a canonical example is the trivial subgroup $\{\mathrm{id}_a\} \leq \mathrm{End}_{\mathbb{A}}(a)$ for an object $a$ in a groupoid $\mathbb{A}$. Importantly, subgroups of endomorphisms in $\mathbb{A}$ can be transferred across morphisms by conjugation: for a morphism $\alpha : a \to a'$ and $G \leq \mathrm{End}(a)$, the conjugate subgroup $\alpha G \alpha^{-1} = \{\alpha g \alpha^{-1} | g \in G\}$ is a subgroup of $\mathrm{End}(a')$.

Our approach involves attaching to a groupoid $\mathbb{A}$ some additional structure which we will call a *kit*, comprising a family of subgroups of endomorphisms for each object.

**Definition 4.1.** A *kit* on a groupoid $\mathbb{A}$ is a family $\mathcal{A} = \{\mathcal{A}(a)\}_{a \in \mathbb{A}}$ consisting of sets $\mathcal{A}(a)$ of subgroups of $\mathrm{End}_{\mathbb{A}}(a)$ that is closed under conjugation; that is, such that, for all $\alpha : a' \to a$ in $\mathbb{A}$, if $G \leq \mathrm{End}(a)$ is in $\mathcal{A}(a)$ then the conjugate subgroup $\alpha^{-1} G \alpha \leq \mathrm{End}(a')$ is in $\mathcal{A}(a')$.

When $\mathcal{A}$ is a *kit* on $\mathbb{A}$, we often refer to the pair $(\mathbb{A}, \mathcal{A})$ as a *kit*, which we also denote by $\mathbb{A}$ for convenience.

**Example 4.2.** Every groupoid $\mathbb{A}$ has the following canonical choices of kits: the trivial one $\mathrm{Triv}_{\mathbb{A}}(a) = \{\mathrm{id}_a\}$, and the maximal one $\mathrm{End}_{\mathbb{A}}(a) = \{G | G \leq \mathrm{End}_{\mathbb{A}}(a)\}$.

As usual with linear logic, our model exhibits several aspects of duality. Every groupoid $\mathbb{A}$ has an *opposite* or *dual* groupoid $\mathbb{A}^{\circ}$, to which it is isomorphic via the mapping $\alpha \mapsto \alpha^{-1}$, and moreover $(\mathbb{A}^{\circ})^{\circ} = \mathbb{A}$; this holds in particular for any group $G$ seen as a one-object groupoid. Observe that for any object $a$ of a groupoid $\mathbb{A}$ one has $\mathrm{End}_{\mathbb{A}^{\circ}}(a) = (\mathrm{End}_{\mathbb{A}^{\circ}}(a))^{\circ}$.

To construct kits on dual groupoids we consider a notion of subgroup orthogonality.

**Definition 4.3.** For a group $G$ and subgroups $H \leq G$ and $K \leq G^{\circ}$, we say that $H$ and $K$ are *orthogonal* if $H \cap K = \{\mathrm{id}\}$, where $\mathrm{id}$ is the identity element in $G$ (and $G^{\circ}$).
From this we get the following construction:

**Lemma 4.4.** For a groupoid $\mathcal{A}$ and a kit $\mathcal{A}$, $\mathcal{A}^{\circ}$ may be equipped with its orthogonal kit $\mathcal{A}^{\perp}$ defined for $a \in \mathcal{A}^{\circ}$ by:

$$ \mathcal{A}^{\perp}(a) = \{G \leq \mathrm{Endo}_{\mathcal{A}^{\circ}}(a) \mid \forall H \in \mathcal{A}(a), G \perp H\}. $$

*Proof.* For the closure under conjugation observe that for a morphism $\alpha : a' \to a$ and subgroups $G \leq \mathrm{Endo}_{\mathcal{A}}(a)$ and $H \leq \mathrm{Endo}_{\mathcal{A}^{\circ}}(a')$, $\alpha^{-1}G \alpha \perp H$ if and only if $G \perp \alpha H \alpha^{-1}$. $\square$

As a basic example observe that, for a groupoid $\mathcal{A}$, the canonical kits from Example 4.2 are orthogonal:

$$ \mathrm{Triv}_{\mathcal{A}}^{\perp} = \mathrm{Endo}_{\mathcal{A}^{\circ}} \qquad \mathrm{Endo}_{\mathcal{A}}^{\perp} = \mathrm{Triv}_{\mathcal{A}^{\circ}}. $$

We define Boolean kits to be those kits which are closed under double orthogonality.

**Definition 4.5.** A Boolean kit $\mathcal{A}$ on a groupoid $\mathcal{A}$ is a kit $(\mathcal{A}, \mathcal{A})$ such that $\mathcal{A} = \mathcal{A}^{\perp\perp}$.

Writing **Kit**($\mathcal{A}$) for the poset of kits on $\mathcal{A}$ under (component-wise) inclusion, the orthogonality relation on kits induces a Galois connection

$$ \begin{array}{ccc} \mathrm{Kit}(\mathcal{A})^{\circ} & \stackrel{(-)^{\perp}}{\longleftrightarrow} & \mathrm{Kit}(\mathcal{A}^{\circ}) \\ \multicolumn{3}{c}{(-)^{\perp}} \end{array} $$

whose fixed points $\mathcal{A} = \mathcal{A}^{\perp\perp}$ are Boolean kits. The requirement that structures be closed under double orthogonality is common in the model theory of linear logic [HS03] and is necessary when one seeks a model for the classical system, in which negation is involutive. More concretely, this condition ensures that certain basic properties always hold for a kit, as we will see shortly.

**Lemma 4.6.** Let $\mathcal{A}, \mathcal{A}'$ be kits on a groupoid $\mathcal{A}$. Then:

(1) $\mathcal{A} \subseteq \mathcal{A}^{\perp\perp}$, where $\subseteq$ is component-wise inclusion.

(2) If $\mathcal{A} \subseteq \mathcal{A}'$ then $\mathcal{A}'^{\perp} \subseteq \mathcal{A}^{\perp}$.

It follows that $\mathcal{A}^{\perp} = \mathcal{A}^{\perp\perp\perp}$; so, in particular, $\mathcal{A}^{\perp}$ is a Boolean kit.

**Lemma 4.7.** Let $(\mathcal{A}, \mathcal{A})$ be a Boolean kit, and let $a \in \mathcal{A}$. Then, for each $a \in \mathcal{A}$, the set $\mathcal{A}(a)$ is closed under subgroups (in particular, $\{\mathrm{id}_a\} \in \mathcal{A}(a)$) and under unions of directed subsets.

*Proof.* Let $H' \leq H \in \mathcal{G}$ and $G \in \mathcal{G}^{\perp}$, then $H' \cap G \subseteq H \cap G = \{\mathrm{id}\}$ which implies that $H' \in \mathcal{G}^{\perp\perp} = \mathcal{G}$. Let $\{G_i\}_{i \in I}$ be a directed family in $\mathcal{G}$, then $\bigcup_{i \in I} G_i$ is a subgroup of $G$ and for $H \in \mathcal{G}^{\perp}$, $(\bigcup_{i \in I} G_i) \cap H = \bigcup_{i \in I} (G_i \cap H) = \{\mathrm{id}\}$ so that $\bigcup_{i \in I} G_i$ is in $\mathcal{G}^{\perp\perp} = \mathcal{G}$ as desired. $\square$

We consider as an example the possible Boolean kits on the group $C_6$, the cyclic group of order 6, seen as a groupoid. For an element $g$ of a group $G$, we denote by $\langle g \rangle$ the cyclic subgroup generated by $g$; that is, $\langle g \rangle = \{g^n \mid n \in \mathbb{Z}\}$. Now, writing $\gamma$ for any generator of $C_6$, it can be verified that the only possible Boolean kits are the maximal and trivial ones, as well as the subsets $\{\langle \gamma^2 \rangle, \{\mathrm{id}\}\}$ and $\{\langle \gamma^3 \rangle, \{\mathrm{id}\}\}$. These form a complete Boolean algebra, and in fact this is the case for the set of Boolean kits on any groupoid.

It is sometimes useful to unfold the condition $\mathcal{A} = \mathcal{A}^{\perp\perp}$ by looking at the family of subsets $\bigcup \mathcal{A}(a) \subseteq \mathrm{Endo}(a)$, for $a \in \mathcal{A}$. This brings us close to Taylor's *creeds* [Tay89], which are subsets of endomorphisms meeting certain explicit closure conditions. In practice, to
show that a kit $\mathcal{A}$ is a Boolean kit, we show that for all $a \in \mathbb{A}$, for all $\alpha \in \bigcup \mathcal{A}(a)^{\perp\perp}$, $\alpha$ is in $\bigcup \mathcal{A}(a)$ which corresponds to the saturation property defined below:

**Definition 4.8.** A kit $\mathcal{A}$ on a groupoid $\mathbb{A}$ is saturated if it satisfies the following condition: for $a \in \mathbb{A}$ and $\alpha \in \mathrm{Endo}(a)$, if the formula $\Phi_{\bigcup \mathcal{A}}(\alpha)$ given by

$$ \forall n \in \mathbb{N}, \alpha^n = \mathrm{id} \lor (\exists m \in \mathbb{N}, \alpha^{nm} \neq \mathrm{id} \land \alpha^{nm} \in \bigcup \mathcal{A}(a)) $$

holds, then $\alpha \in \bigcup \mathcal{A}(a)$.

Saturation is however not enough to prove $\mathcal{A} = \mathcal{A}^{\perp\perp}$, it only shows that $\bigcup \mathcal{A}(a) = \bigcup \mathcal{A}^{\perp\perp}(a)$ for all $a \in \mathbb{A}$. We need further that $\mathcal{A}(a) = \{H \leq \mathbb{A}(a, a) | H \subseteq \bigcup \mathcal{A}(a)\}$ for all $a \in \mathbb{A}$.

**Lemma 4.9.** For a groupoid $\mathbb{A}$ and a kit $\mathcal{A}$ on $\mathbb{A}$, $\mathcal{A} = \mathcal{A}^{\perp\perp}$ if and only if

(1) for all $a \in \mathbb{A}$, $\mathcal{A}(a) = \{H \leq \mathbb{A}(a, a) | H \subseteq \bigcup \mathcal{A}(a)\}$

(2) $\mathcal{A}$ is saturated.

*Proof.* Assume that $\mathcal{A} = \mathcal{A}^{\perp\perp}$ and let $H \leq \mathbb{A}(a, a)$ be such that $H \subseteq \bigcup \mathcal{A}(a)$ i.e. for all $\alpha \in H$, $\langle\alpha\rangle$ is in $\mathcal{A}(a)$ since $\mathcal{A}(a)$ is downclosed by Lemma 4.7. Let $K$ be in $\mathcal{A}^{\perp}(a)$, for any $\alpha \in H \cap K$, we have $\langle\alpha\rangle \cap K = \{\mathrm{id}\}$ which implies that $H$ is in $\mathcal{A}^{\perp\perp}(a) = \mathcal{A}(a)$ so that $\mathcal{A}(a) = \{H \leq \mathbb{A}(a, a) | H \subseteq \bigcup \mathcal{A}(a)\}$ as desired. The saturation property is an immediate unfolding of the double orthogonality. For the other direction, if $\mathcal{A}$ is saturated, we have $\bigcup \mathcal{A}(a) = \bigcup \mathcal{A}^{\perp\perp}(a)$ for all $a \in \mathbb{A}$ which implies that $\mathcal{A} = \mathcal{A}^{\perp\perp}$ by (1). $\square$

For a kit $(\mathbb{A}, \mathcal{A})$ we will use the notation $(\mathbb{A}, \mathcal{A})^{\perp} = (\mathbb{A}^{\circ}, \mathcal{A}^{\perp})$, and continue to use underline symbols $\underline{\mathbb{A}}$, $\underline{\mathbb{B}}$, for pairs $(\mathbb{A}, \mathcal{A})$, $(\underline{\mathbb{B}}, \underline{\mathbb{B}})$.

**4.2. Stabilized Profunctors.** For groupoids equipped with kits, we will consider certain constrained profunctors which we call stabilized.

**Definition 4.10.** For kits $(\mathbb{A}, \mathcal{A})$ and $(\underline{\mathbb{B}}, \underline{\mathbb{B}})$, a stabilized profunctor $P : (\mathbb{A}, \mathcal{A}) \dashrightarrow (\underline{\mathbb{B}}, \underline{\mathbb{B}})$ is a profunctor $P : \mathbb{A} \dashrightarrow \underline{\mathbb{B}}$ such that, for all $a \in \mathbb{A}$, $b \in \underline{\mathbb{B}}$, $p \in P(b, a)$, $\alpha \in \mathrm{Endo}(a)$, $\beta \in \mathrm{Endo}(b)$, if $\alpha \cdot p \cdot \beta = p$ then

$$ \alpha \in \bigcup \mathcal{A}(a) \implies \beta \in \bigcup \mathcal{B}(b) \text{ and } \beta \in \bigcup \mathcal{B}^{\perp}(b) \implies \alpha \in \bigcup \mathcal{A}^{\perp}(a). $$

It is instructive to consider some examples.

**Example 4.11.** (1) Any profunctor $P : \mathbb{A} \dashrightarrow \underline{\mathbb{B}}$ is a stabilized profunctor $P : (\mathbb{A}, \mathrm{Triv}_{\mathbb{A}}) \dashrightarrow (\underline{\mathbb{B}}, \mathrm{Endo}_{\underline{\mathbb{B}}})$.

(2) A stabilized profunctor $(\mathbb{A}, \mathrm{Endo}_{\mathbb{A}}) \dashrightarrow (\underline{\mathbb{B}}, \mathrm{Endo}_{\underline{\mathbb{B}}})$ is a profunctor $P : \mathbb{A} \dashrightarrow \underline{\mathbb{B}}$ that acts freely on $\mathbb{A}$. In other words, for all $a \in \mathbb{A}$, $b \in \underline{\mathbb{B}}$, $p \in P(b, a)$, $\alpha \in \mathrm{Endo}(a)$, if $\alpha \cdot p = p$ then $\alpha = \mathrm{id}_a$.

(3) For any kit $\underline{\mathbb{A}} = (\mathbb{A}, \mathcal{A})$, the identity $\mathrm{y} : \mathbb{A}^{\circ} \times \mathbb{A} \to \mathrm{Set} : (a, a') \mapsto \mathbb{A}(a, a')$ is a stabilized profunctor $\underline{\mathbb{A}} \dashrightarrow \underline{\mathbb{A}}$. This is because, for $a, a' \in \mathbb{A}$, $\alpha \in \mathrm{Endo}(a)$, $\alpha' \in \mathrm{Endo}(a')$, and $\gamma \in \mathbb{A}(a, a')$, $\alpha' \cdot \gamma \cdot \alpha = \alpha' \circ \gamma \circ \alpha = \gamma$ implies that $\alpha$ and $\alpha'$ are conjugate; and both $\mathcal{A}$ and $\mathcal{A}^{\perp}$ are closed under conjugation.

Stabilized profunctors are closed under composition:

**Lemma 4.12.** For kits $(\mathbb{A}, \mathcal{A})$, $(\underline{\mathbb{B}}, \underline{\mathbb{B}})$ and $(\mathbb{C}, \mathcal{C})$, if $P : (\mathbb{A}, \mathcal{A}) \dashrightarrow (\underline{\mathbb{B}}, \underline{\mathbb{B}})$ and $Q : (\underline{\mathbb{B}}, \underline{\mathbb{B}}) \dashrightarrow (\mathbb{C}, \mathcal{C})$ are stabilized profunctors, then their composite $Q \circ P$ is an stabilized profunctor $(\mathbb{A}, \mathcal{A}) \dashrightarrow (\mathbb{C}, \mathcal{C})$.
**Proof.** Let $a \in \mathbb{A}$, $c \in \mathbb{C}$, $\alpha \in \mathbb{A}(a, a)$, $\gamma \in \mathbb{C}(c, c)$ and $t \in (Q \circ P)(c, a)$ be such that $\alpha \cdot t \cdot \gamma = t$. The element $t$ is of the form $p \ltimes q \in \int^b P(b, a) \times Q(c, b)$ for some $b \in \mathbb{B}$, $p \in P(b, a)$ and $q \in Q(c, b)$ so $\alpha \cdot t \cdot \gamma = t$ is equivalent to $(\alpha \cdot p) \ltimes (q \cdot \gamma) = p \ltimes q$ which implies that there exists $\beta \in \mathbb{B}(b, b)$ such that $\alpha \cdot p \cdot \beta = p$ and $\beta^{-1} \cdot q \cdot \gamma = q$. If $\alpha \in \bigcup \mathcal{A}(a)$ then since $P$ is a stabilized profunctor and $\alpha \cdot p \cdot \beta = p$, we have $\beta \in \bigcup \mathcal{B}(b)$ which implies that $\beta^{-1} \in \bigcup \mathcal{B}(b)$ by closure under powers ($\beta$ is an element of a group $G \in \mathcal{B}(b)$). Likewise, since $Q$ is a stabilized profunctor and $\beta^{-1} \cdot q \cdot \gamma = q$, we have $\gamma \in \bigcup \mathcal{C}(c)$. The other implication $\gamma \in \bigcup \mathcal{C}^{\perp}(c) \Rightarrow \alpha \in \bigcup \mathcal{A}^{\perp}(a)$ is shown similarly. $\square$

Boolean kits, stabilized profunctors, and natural transformations assemble into a bcategory which we denote **SProf**.

**Definition 4.13.** The dual of a profunctor $P: \mathbb{A} \dashrightarrow \mathbb{B}$ is the profunctor $P^{\circ}: \mathbb{B}^{\circ} \dashrightarrow \mathbb{A}^{\circ}$ given by:

$$ (a, b) \mapsto P(b, a). $$

This induces a self-duality $(-)^{\perp}: \mathbf{Prof}^{\circ} \to \mathbf{Prof}$.

The following observation is immediate from the definition: if $P$ is a stabilized profunctor $\mathbb{A} \dashrightarrow \mathbb{B}$ then $P^{\circ}$ is a stabilized profunctor $\mathbb{B}^{\perp} \dashrightarrow \mathbb{A}^{\perp}$, and indeed the dualisation operation on kits $\mathbb{A} \mapsto \mathbb{A}^{\perp}$ induces a self-duality on **SProf**.

The additional structure may be forgotten through a collapse:

**Proposition 4.14.** There is a forgetful pseudo-functor **SProf** $\to$ **Prof** which is strict, faithful and locally full and faithful; that is, for kits $(\mathbb{A}, \mathcal{A})$ and $(\mathbb{B}, \mathcal{B})$, the induced functor **SProf**(($(\mathbb{A}, \mathcal{A})$), $(\mathbb{B}, \mathcal{B})$) $\to$ **Prof**$(\mathbb{A}, \mathbb{B})$ is injective on objects and fully faithful.

## 5. LOGICAL STRUCTURE OF STABILIZED PROFUNCTORS

We show that **SProf** is a model of classical linear logic, and that this structure extends and refines that of **Prof**. In this section we focus on multiplicative and additive structure. The exponential modality will be discussed in the next section.

### 5.1. Biproduct structure.
In the standard 1-dimensional models of stability (coherence spaces, probabilistic coherence spaces, etc.), the linear categories do not have biproducts which implies in particular that they are not models of differential linear logic. In our setting, the biproduct structure in **Prof** can be transported to **SProf**. For a family of groupoids $(\mathbb{A}_i)_{i \in I}$, we denote by $\&_{i \in I} \mathbb{A}_i$ their coproduct in **Cat**, whose objects are given by the disjoint union $\coprod_{i \in I} \{i\} \times \mathbb{A}_i$. In **Prof**, this is a biproduct, meaning that $\&_{i \in I} \mathbb{A}_i$ is a product and a coproduct for the family $(\mathbb{A}_i)_{i \in I}$.

For a finite family of kits $\{\mathbb{A}_i = (\mathbb{A}_i, \mathcal{A}_i)\}_{i \in I}$, the categorical coproduct $\&_{i \in I} \mathbb{A}_i$ has a canonical kit structure $(\&_{i \in I} \mathbb{A}_i, \coprod_{i \in I} \mathcal{A}_i)$ defined as $(\coprod_{i \in I} \mathcal{A}_i)(j, a) = \mathcal{A}_j(a)$ for all $j \in I$, $a \in \mathbb{A}$. Since $(\coprod_{i \in I} \mathbb{A}_i)^{\perp} = \coprod_{i \in I} \mathcal{A}_i$, it is in fact a Boolean kit which implies that the product kit $\&_{i \in I} \mathbb{A}_i := (\&_{i \in I} \mathbb{A}_i, \coprod_{i \in I} \mathcal{A}_i)$ is equal to the coproduct kit $\oplus_{i \in I} \mathbb{A}_i := (\&_{i \in I} \mathbb{A}_i)^{\perp}$.

The projections $\pi_j: \&_{i \in I} \mathbb{A}_i \dashrightarrow \mathbb{A}_j$ in **Prof** determine stabilized profunctors $\&_{i \in I} \mathbb{A}_i \dashrightarrow \mathbb{A}_j$, and one can show the existence of an adjoint equivalence

$$ \prod_{i \in I} \mathbf{SProf}(\mathbb{B}, \mathbb{A}_{i \in I}) \simeq \mathbf{SProf}(\mathbb{B}, \&_{i \in I} \mathbb{A}_i) $$
making $\&_{i \in I} \underline{\mathcal{A}}_i$ a bicategorical product. From the self-dual structure of **SProf**, we obtain that the inclusions $\mathrm{in}_j : \underline{\mathcal{A}}_j \to \&_{i \in I} \underline{\mathcal{A}}_i$, obtained as the dual of the projection $\pi_j : \&_{i \in I} \underline{\mathcal{A}}_i \to \underline{\mathcal{A}}_j$, are also stabilized profunctors and yield the desired adjoint equivalence in **SProf** for coproducts. We thus have finite biproducts, with the zero object defined by the kit $(0, \emptyset)$ on the empty groupoid **0**.

**5.2. *-Autonomous structure.**** The bicategory **Prof** can be equipped with a symmetric monoidal structure defined by the cartesian product of categories $\mathcal{A} \otimes \mathcal{B} = \mathcal{A} \times \mathcal{B}$, with monoidal unit given by the terminal category **1**. Additionally, the duality pseudo-functor $\mathcal{A} \to \mathcal{A}^\circ$ makes **Prof** a compact closed bicategory [Sta16]. From the point of view of linear logic, **Prof** is a degenerate model: $(\mathcal{A}^\perp \otimes \mathcal{B}^\perp)^\perp = \mathcal{A} \otimes \mathcal{B}$, hence the multiplicative connectives $\mathcal{Y}$ and $\otimes$ are identified. The addition of kits to groupoids eliminates this degeneracy: **SProf** is not compact closed but merely *-autonomous, as we will see.

For kits $(\mathcal{A}, \mathcal{A})$ and $(\mathcal{B}, \mathcal{B})$, we construct a tensor product as

$$ (\mathcal{A}, \mathcal{A}) \otimes (\mathcal{B}, \mathcal{B}) := (\mathcal{A} \times \mathcal{B}, (\mathcal{A} \times \mathcal{B})^{\perp}) $$

where for $a \in \mathcal{A}$ and $b \in \mathcal{B}$, $(\mathcal{A} \times \mathcal{B})(a, b) := \mathcal{A}(a) \times \mathcal{B}(b)$. The closure under double orthogonality is necessary because $\mathcal{A} \times \mathcal{B}$ is not a Boolean kit in general. The monoidal unit is the kit $(\mathbf{1}, \mathrm{Triv}_1)$. To show that this induces a symmetric monoidal structure, it suffices to show that the symmetric monoidal structure of **Prof** lifts to **SProf**, i.e. that associator, braiding, and left and right unitors are pseudo-natural transformations with components in **SProf**, and that the tensor product is a pseudo-functor $\mathbf{SProf} \times \mathbf{SProf} \to \mathbf{SProf}$. All coherence axioms will then follow from the (faithful) forgetful pseudo-functor $\mathbf{SProf} \to \mathbf{Prof}$.

This way, we avoid much of the work in defining a bicategorical monoidal structure. The proof is not automatic, however: our use of the closure operator $(-)^{\perp\perp}$ in the definition of $\otimes$ makes certain properties, e.g. associativity, difficult to verify. The following lemma is a key tool in this process.

**Lemma 5.1.** For Boolean kits $\underline{\mathcal{A}} = (\mathcal{A}, \mathcal{A})$ and $\underline{\mathcal{B}} = (\mathcal{B}, \mathcal{B})$, define the kit $\underline{\mathcal{A}} \to \underline{\mathcal{B}}$ as $(\mathcal{A}^\circ \times \mathcal{B}, \mathcal{A} \to \mathcal{B})$ where $(\mathcal{A} \to \mathcal{B})(a, b)$ is the set of all subgroups $H \le \mathrm{End}(a, b)$ such that:

$$ \forall (\alpha, \beta) \in H, \alpha \in \bigcup \mathcal{A}(a) \implies \beta \in \bigcup \mathcal{B}(b) \text{ and } \beta \in \bigcup \mathcal{B}^{\perp}(b) \implies \alpha \in \bigcup \mathcal{A}^{\perp}(a). $$

The kit $\underline{\mathcal{A}} \to \underline{\mathcal{B}}$ is Boolean.

*Proof.* To prove that $\underline{\mathcal{A}} \to \underline{\mathcal{B}}$ forms a Boolean kit, we first show that for objects $a \in \mathcal{A}, b \in \mathcal{B}$ and subgroups $K \in \mathcal{A}(a)$ and $G \in \mathcal{B}^{\perp}(b)$, we have $K \times G \in (\mathcal{A} \to \mathcal{B})^{\perp}(a, b)$. Let $H$ be in $(\mathcal{A} \to \mathcal{B})(a, b)$ and $(\alpha, \beta) \in (K \times G) \cap H$. Since $\alpha \in K \in \mathcal{A}(a)$, we have $\beta \in \mathcal{B}(b)$ by definition of $\mathcal{A} \to \mathcal{B}$ which implies that $\beta = \mathrm{id}$ since $\beta \in G \in \mathcal{B}^{\perp}(b)$. Likewise, since $\beta \in G \in \mathcal{B}^{\perp}(b)$, we have $\alpha \in \mathcal{A}^{\perp}(a)$ which implies that $\alpha = \mathrm{id}$ as $\alpha \in K \in \mathcal{A}(a)$.

Now, let $H$ be in $(\mathcal{A} \to \mathcal{B})^{\perp\perp}(a, b)$, we show that $H$ is in $(\mathcal{A} \to \mathcal{B})(a, b)$. Let $(\alpha, \beta)$ be in $H$ and assume that $\alpha \in \bigcup \mathcal{A}(a)$ and that there exists $n \in \mathbb{N}$ such that $\beta^n \in \bigcup \mathcal{B}^{\perp}(b)$. Hence, we have $\langle \alpha^n \rangle \times \langle \beta^n \rangle \in (\mathcal{A}(a) \times \mathcal{B}^{\perp}(b))$ which implies that $\langle \alpha^n \rangle \times \langle \beta^n \rangle \in (\mathcal{A} \to \mathcal{B})^{\perp}(a, b)$ so that $\alpha^n = \mathrm{id}$ and $\beta^n = \mathrm{id}$ as desired. We can show similarly that if $\beta \in \bigcup \mathcal{B}^{\perp}(b)$ then $\alpha \in \bigcup \mathcal{A}^{\perp}(a)$.

For a subgroup $H \le \mathrm{End}(a, b)$ such that $H \subseteq \bigcup (\mathcal{A} \to \mathcal{B})(a, b)$, it is immediate that $H$ is in $(\mathcal{A} \to \mathcal{B})(a, b)$. Hence, by Lemma 4.9, we conclude that $\mathcal{A} \to \mathcal{B}$ is a kit. $\square$

As an immediate corollary, we obtain:
**Corollary 5.2.** For Boolean kits $\mathbf{A}$ and $\mathbf{B}$, the categories $\mathbf{SProf}(\mathbf{A}, \mathbf{B})$ and $\mathbf{SProf}(\mathbf{1}, \mathbf{A} \to \mathbf{B})$ are isomorphic.

**Lemma 5.3.** If $P_1 : \mathbf{A}_1 \to \mathbf{B}_1$ and $P_2 : \mathbf{A}_2 \to \mathbf{B}_2$ are stabilized profunctors then so is $P_1 \otimes P_2 : (\mathbf{A}_1 \otimes \mathbf{A}_2) \to (\mathbf{B}_1 \otimes \mathbf{B}_2)$ defined as

$$ (P_1 \otimes P_2)((b_1, b_2), (a_1, a_2)) := P_1(b_1, a_1) \times P_2(b_2, a_2). $$

*Proof.* Assume that there is $(a_1, a_2) \in \mathbf{A}_1 \times \mathbf{A}_2$, $(b_1, b_2) \in \mathbf{B}_1 \times \mathbf{B}_2$, $(\alpha_1, \alpha_2) \in \text{Endo}(a_1, a_2)$, $(\beta_1, \beta_2) \in \text{Endo}(b_1, b_2)$ and $(p_1, p_2) \in P_1(b_1, a_1) \times P_2(b_2, a_2)$ such that

$$ (\alpha_1, \alpha_2) \cdot (p_1, p_2) \cdot (\beta_1, \beta_2) = (p_1, p_2) $$

i.e. $\alpha_1 \cdot p_1 \cdot \beta_1 = p_1$ and $\alpha_2 \cdot p_2 \cdot \beta_2 = p_2$.

* We first show that if $(\alpha_1, \alpha_2) \in \bigcup(\mathbf{A}_1 \otimes \mathbf{A}_2)(a_1, a_2)$ then $(\beta_1, \beta_2) \in \bigcup(\mathbf{B}_1 \otimes \mathbf{B}_2)(b_1, b_2)$.

Recall from Definition 4.8 that $(\alpha_1, \alpha_2) \in \bigcup(\mathbf{A}_1 \otimes \mathbf{A}_2)(a_1, a_2) = \bigcup(\mathbf{A}_1 \times \mathbf{A}_2)^{\perp\perp}(a_1, a_2)$ is equivalent to the formula $\Phi_{\bigcup \mathbf{A}_1 \otimes \mathbf{A}_2}(\alpha_1, \alpha_2)$ given by:

$$ \forall n \in \mathbb{N}, (\alpha_1, \alpha_2)^n = (\text{id}, \text{id}) \lor \quad (\exists m \in \mathbb{N}, (\text{id}, \text{id}) \neq (\alpha_1, \alpha_2)^{nm} \in \bigcup(\mathbf{A}_1 \times \mathbf{A}_2)(a_1, a_2)). $$

Let $n \in \mathbb{N}$ be such that $\beta_1^n \neq \text{id}$ or $\beta_2^n \neq \text{id}$. If $(\alpha_1, \alpha_2)^n = (\text{id}, \text{id})$, then $(\alpha_1^n, \alpha_2^n) \in \bigcup(\mathbf{A}_1 \times \mathbf{A}_2)(a_1, a_2)$ which implies that $(\beta_1^n, \beta_2^n) \in \bigcup(\mathbf{B}_1 \times \mathbf{B}_2)(b_1, b_2)$ since $P_1$ and $P_2$ are stabilized profunctors. Taking $m = 1$, the formula $\Phi_{\bigcup \mathbf{B}_1 \otimes \mathbf{B}_2}(\beta_1, \beta_2)$ holds.

Assume now that there exists $m \in \mathbb{N}$ such that $(\alpha_1^{nm}, \alpha_2^{nm}) \neq (\text{id}, \text{id})$ and $(\alpha_1^{nm}, \alpha_2^{nm}) \in \bigcup(\mathbf{A}_1 \times \mathbf{A}_2)(a_1, a_2)$. It implies that $(\beta_1^{nm}, \beta_2^{nm})$ is in $\bigcup(\mathbf{B}_1 \times \mathbf{B}_2)(b_1, b_2)$ since $P_1$ and $P_2$ are stabilized profunctors. Assume that $\beta_1^{nm} = \text{id}$ and $\beta_2^{nm} = \text{id}$, then $(\beta_1^{nm}, \beta_2^{nm}) \in \bigcup(\mathbf{B}_1^{\perp} \times \mathbf{B}_2^{\perp})(b_1, b_2)$ which implies that $(\alpha_1^{nm}, \alpha_2^{nm}) \in \bigcup(\mathbf{A}_1^{\perp} \times \mathbf{A}_2^{\perp})(a_1, a_2)$. Hence, $(\alpha_1^{nm}, \alpha_2^{nm}) = (\text{id}, \text{id})$ which gives us the desired contradiction.

* For the other direction, assume that $(\beta_1, \beta_2) \in \bigcup(\mathbf{B}_1 \otimes \mathbf{B}_2)^{\perp}(b_1, b_2) = \bigcup(\mathbf{B}_1 \times \mathbf{B}_2)^{\perp}(b_1, b_2)$, we want to show that $(\alpha_1, \alpha_2) \in \bigcup(\mathbf{A}_1 \times \mathbf{A}_2)^{\perp}(a_1, a_2)$. Let $H_1 \in \mathbf{A}_1(a_1)$, $H_2 \in \mathbf{A}_2(a_2)$ and $n \in \mathbb{N}$ such that $(\alpha_1^n, \alpha_2^n) \in H_1 \times H_2$. We need to show that $(\alpha_1^n, \alpha_2^n) = (\text{id}, \text{id})$. Since $P_1$ is a stabilized profunctor, $\beta_1^n \in \bigcup \mathbf{B}_1(b_1)$, and therefore, by Corollary 5.5, we must have $\beta_2^n \in \bigcup \mathbf{B}_2(b_2)^{\perp}$. Since $P_2$ is a stabilized profunctor, we must have $\alpha_2^n \in \mathbf{A}_2(a_2)^{\perp}$, and therefore $\alpha_2^n = \text{id}$. Likewise, we can show that $\alpha_1^n = \text{id}$ so that $(\alpha_1^n, \alpha_2^n) = (\text{id}, \text{id})$ as desired. $\square$

From this, one derives that $\otimes$ defines a pseudo-functor of two arguments. Continuing with the monoidal structure, we turn to the unitors. For a kit $\mathbf{A} = (\mathbf{A}, \mathbf{A})$, the canonical isomorphisms $\mathbf{1} \times \mathbf{A} \cong \mathbf{A}$ and $\mathbf{A} \times \mathbf{1} \cong \mathbf{A}$ in **Cat** induce adjoint equivalences $\mathbf{1} \otimes \mathbf{A} \to \mathbf{A}$ and $\mathbf{A} \otimes \mathbf{1} \to \mathbf{A}$ in $\mathbf{SProf}$ that are pseudo-natural in $\mathbf{A}$. Next, for kits $\mathbf{A}$ and $\mathbf{B}$, the component of the braiding $\sigma_{\mathbf{A},\mathbf{B}} : \mathbf{A} \times \mathbf{B} \to \mathbf{B} \times \mathbf{A}$ in **Prof** is a stabilized profunctor $\mathbf{A} \otimes \mathbf{B} \to \mathbf{B} \otimes \mathbf{A}$ and it induces a pseudo-natural family of adjoint equivalences in $\mathbf{SProf}$.

**Lemma 5.4.** For Boolean kits $\mathbf{A} = (\mathbf{A}, \mathbf{A})$ and $\mathbf{B} = (\mathbf{B}, \mathbf{B})$, the Boolean kits $\mathbf{A} \to \mathbf{B}$ and $(\mathbf{A} \otimes \mathbf{B}^{\perp})^{\perp}$ are isomorphic.

*Proof.* Let $a \in \mathbf{A}$, $b \in \mathbf{B}$ and $(\alpha, \beta) \in \bigcup(\mathbf{A} \otimes \mathbf{B}^{\perp})^{\perp}(a, b) = \bigcup(\mathbf{A}(a) \times \mathbf{B}(b)^{\perp})^{\perp}$. Assume that $\alpha \in \bigcup \mathbf{A}(a)$, if there exists $n \in \mathbb{N}$ such that $\beta^n \in \bigcup \mathbf{B}^{\perp}(b)$, then $(\alpha, \beta)^n \in \bigcup(\mathbf{A}(a) \times \mathbf{B}(b)^{\perp})$ which implies that $(\alpha, \beta)^n = (\text{id}, \text{id})$ so that $\beta$ is in $\bigcup \mathbf{B}(b)$ as desired. Dually, assume that $\beta \in \bigcup \mathbf{B}^{\perp}(b)$, if there exists $n \in \mathbb{N}$ such that $\alpha^n \in \bigcup \mathbf{A}^{\perp}(a)$ then $(\alpha, \beta)^n = (\text{id}, \text{id})$ which implies that $\alpha \in \bigcup \mathbf{A}^{\perp\perp}(a) = \bigcup \mathbf{A}(a)$ as desired.
For the other inclusion, let $H \in (\mathcal{A} \to \mathcal{B})(a, b)$, $K \in \mathcal{A}(a)$, $G \in \mathcal{B}^{\perp}(b)$ and $(\alpha, \beta) \in H \cap (K \times G)$. Since $\alpha$ is in $H \in \mathcal{A}(a)$ and $(\alpha, \beta) \in \bigcup (\mathcal{A} \to \mathcal{B})(a, b)$, we have $\beta \in \bigcup \mathcal{B}(b)$ which implies that $\beta = \text{id}$ as $\beta$ is in $G \in \mathcal{B}^{\perp}(b)$. We obtain similarly that $\alpha = \text{id}$ which implies that $G$ is in $(\mathcal{A}(a) \times \mathcal{B}(b)^{\perp})^{\perp}$. $\square$

**Corollary 5.5.** For Boolean kits $(\mathcal{A}, \mathcal{A})$ and $(\mathcal{B}, \mathcal{B})$, objects $a \in \mathcal{A}$ and $b \in \mathcal{B}$, if $(\alpha, \beta) \in \bigcup (\mathcal{A}(a) \times \mathcal{B}(b))^{\perp}$, then $\alpha \in \bigcup \mathcal{A}(a)$ implies $\beta \in \bigcup \mathcal{B}(b)^{\perp}$ and $\beta \in \bigcup \mathcal{B}(b)$ implies $\alpha \in \bigcup \mathcal{A}(a)^{\perp}$.

**Lemma 5.6.** For Boolean kits $\underline{\mathcal{A}}, \underline{\mathcal{B}}$ and $\underline{\mathcal{C}}$, the Boolean kits $(\underline{\mathcal{A}} \otimes \underline{\mathcal{B}}) \to \underline{\mathcal{C}}$ and $\underline{\mathcal{A}} \to (\underline{\mathcal{B}} \to \underline{\mathcal{C}})$ are isomorphic.

*Proof.* We show that for objects $a \in \mathcal{A}$, $b \in \mathcal{B}$ and $c \in \mathcal{C}$, we have:

$$((\mathcal{A}(a) \times \mathcal{B}(b))^{\perp \perp} \times \mathcal{C}^{\perp}(c))^{\perp} \cong ((\mathcal{A}(a) \times \mathcal{B}(b)) \times \mathcal{C}^{\perp}(c))^{\perp} \quad \text{and} \\ (\mathcal{A}(a) \times (\mathcal{B}(b) \times \mathcal{C}^{\perp}(c))^{\perp \perp})^{\perp} \cong (\mathcal{A}(a) \times (\mathcal{B}(b) \times \mathcal{C}^{\perp}(c)))^{\perp}.$$

Since $\mathcal{A}(a) \times \mathcal{B}(b) \subseteq (\mathcal{A}(a) \times \mathcal{B}(b))^{\perp \perp}$, we have $(\mathcal{A}(a) \times \mathcal{B}(b)) \times \mathcal{C}^{\perp}(c) \subseteq (\mathcal{A}(a) \times \mathcal{B}(b))^{\perp \perp} \times \mathcal{C}^{\perp}(c)$ which implies that

$$((\mathcal{A}(a) \times \mathcal{B}(b))^{\perp \perp} \times \mathcal{C}^{\perp}(c))^{\perp} \subseteq ((\mathcal{A}(a) \times \mathcal{B}(b)) \times \mathcal{C}^{\perp}(c))^{\perp}.$$

For the reverse inclusion, let $G$ be in $((\mathcal{A}(a) \times \mathcal{B}(b)) \times \mathcal{C}^{\perp}(c))^{\perp}$ and $H$ in $(\mathcal{A}(a) \times \mathcal{B}(b))^{\perp \perp} \times \mathcal{C}^{\perp}(c)$ i.e. $H = H_1 \times H_2$ with $H_1 \in (\mathcal{A}(a) \times \mathcal{B}(b))^{\perp \perp}$ and $H_2 \in \mathcal{C}^{\perp}(c)$. To show that $G \perp H$, assume that there exists $((\alpha_1, \alpha_2), \alpha_3) \in G \cap H$. Then, $\alpha_3 \in H_2 \in \mathcal{C}^{\perp}(c)$ so by Corollary 5.5, we have $(\alpha_1, \alpha_2) \in (\mathcal{A}(a) \times \mathcal{B}(b))^{\perp}$. Since $(\alpha_1, \alpha_2) \in H_1 \in (\mathcal{A}(a) \times \mathcal{B}(b))^{\perp \perp}$, we must have $\alpha_1 = \text{id}$ and $\alpha_2 = \text{id}$. Hence, $(\alpha_1, \alpha_2) \in \mathcal{A}(a) \times \mathcal{B}(b)$ so by Corollary 5.5 again, we have $\alpha_3 \in \mathcal{C}^{\perp \perp}(c)$ which implies that $\alpha_3 = \text{id}$ as desired.

The isomorphism $((\mathcal{A}(a) \times (\mathcal{B}(b) \times \mathcal{C}^{\perp}(c))^{\perp \perp})^{\perp}) \cong ((\mathcal{A}(a) \times (\mathcal{B}(b) \times \mathcal{C}^{\perp}(c)))^{\perp})^{\perp}$ is derived using a similar argument. $\square$

**Lemma 5.7.** For Boolean kits $(\mathcal{A}, \mathcal{A})$, $(\mathcal{B}, \mathcal{B})$ and $(\mathcal{C}, \mathcal{C})$, the component of the associator $\alpha_{\mathcal{A},\mathcal{B},\mathcal{C}}$ in **Prof** is a stabilized profunctor

$$((\mathcal{A}, \mathcal{A}) \otimes (\mathcal{B}, \mathcal{B})) \otimes (\mathcal{C}, \mathcal{C}) \dashrightarrow (\mathcal{A}, \mathcal{A}) \otimes ((\mathcal{B}, \mathcal{B}) \otimes (\mathcal{C}, \mathcal{C}))$$

inducing a family of adjoint equivalences pseudo-natural in $(\mathcal{A}, \mathcal{A})$, $(\mathcal{B}, \mathcal{B})$, and $(\mathcal{C}, \mathcal{C})$.

*Proof.* It suffices to show that the Boolean kits $(\underline{\mathcal{A}} \otimes \underline{\mathcal{B}}) \otimes \underline{\mathcal{C}}$ and $\underline{\mathcal{A}} \otimes (\underline{\mathcal{B}} \otimes \underline{\mathcal{C}})$ are isomorphic. By Lemmas 5.4 and 5.6, we have:

$$\begin{align*}
(\underline{\mathcal{A}} \otimes \underline{\mathcal{B}}) \otimes \underline{\mathcal{C}} &\cong ((\underline{\mathcal{A}} \otimes \underline{\mathcal{B}}) \to \underline{\mathcal{C}}^{\perp})^{\perp} \cong (\underline{\mathcal{A}} \to (\underline{\mathcal{B}} \to \underline{\mathcal{C}}^{\perp}))^{\perp} \\
&\cong (\underline{\mathcal{A}} \to (\underline{\mathcal{B}} \otimes \underline{\mathcal{C}})^{\perp})^{\perp} \cong \underline{\mathcal{A}} \otimes (\underline{\mathcal{B}} \otimes \underline{\mathcal{C}}).
\end{align*}$$

**Proposition 5.8.** The bicategory **SProf** is symmetric monoidal.

Finally, **SProf** is *-autonomous* [Bar06]:

**Proposition 5.9.** For Boolean kits $\underline{\mathcal{A}}, \underline{\mathcal{B}}$, and $\underline{\mathcal{C}}$ there is a pseudo-natural adjoint equivalence

$$\mathbf{SProf}(\underline{\mathcal{A}} \otimes \underline{\mathcal{B}}, \underline{\mathcal{C}}^{\perp}) \cong \mathbf{SProf}(\underline{\mathcal{A}}, (\underline{\mathcal{B}} \otimes \underline{\mathcal{C}})^{\perp}).$$

*Proof.* By Corollary 5.2, it suffices to show that $(\underline{\mathcal{A}} \otimes \underline{\mathcal{B}}) \to \underline{\mathcal{C}}^{\perp} \cong \underline{\mathcal{B}} \to (\underline{\mathcal{B}} \otimes \underline{\mathcal{C}})^{\perp}$ which we obtain from Lemmas 5.4 and 5.6. $\square$
It follows that the symmetric monoidal bicategory **SProf** has closed structure given by $\mathbb{A} \to \mathbb{B} = (\mathbb{A} \otimes \mathbb{B}^{\perp})^{\perp}$, and that the object $\perp = \mathbf{1}^{\perp} \cong \mathbf{1}$ is dualising: the canonical stabilized profunctor $\mathbb{A} \to (\mathbb{A} \to \perp) \to \perp$ is part of an equivalence representing the involutive negation of classical linear logic.

Moreover, the operation $\mathbb{A} \mathfrak{N} \mathbb{B} := (\mathbb{A}^{\perp} \otimes \mathbb{B}^{\perp})^{\perp}$ gives rise to a second monoidal structure on **SProf** distinct from the tensor $\otimes$; in the compact closed **Prof** these degenerate to the same structure. Finally, we have the additional property that $\mathcal{A} \mathfrak{N} \mathcal{B} = (\mathcal{A}^{\perp} \times \mathcal{B}^{\perp})^{\perp}$ is a (component-wise) subset of $\mathcal{A} \otimes \mathcal{B} = (\mathcal{A} \times \mathcal{B})^{\perp}$, making **SProf** a model for the *mix* rule [CS97].

## 6. STABLE SPECIES

As described in Section 3.2, the bicategory **Esp** of generalized species of structures arises as a coKleisli construction over the bicategory **Prof**, for the pseudo-comonad $\Sigma$, where $\Sigma\mathbb{A}$ is the symmetric strict monoidal completion of $\mathbb{A}$.

**6.1. Exponential structure.** We proceed to extend the $\Sigma$ construction to **SProf**. We show that this determines a linear exponential pseudo-comonad, whose coKleisli bicategory is that of *stable species of structures*. With an eye to linear logic, we call this extension !, so that for every $(\mathbb{A}, \mathcal{A}) \in \mathbf{SProf}$ one has

$$ ! ( \mathbb{A}, \mathcal{A} ) := ( \Sigma \mathbb{A}, ! \mathcal{A} ) $$

and we will define the Boolean kit $!\mathcal{A}$ shortly.

Consider an object $u = \langle a_1, \dots, a_n \rangle \in \Sigma\mathbb{A}$ and an element $\alpha = (\sigma, (\alpha_i : a_i \to a_{\sigma(i)})_{i \in [n]})$ of $\text{End}_{\Sigma\mathbb{A}}(u)$. Unless the permutation $\sigma$ is the identity, the morphisms $\alpha_i$ are not endomorphisms. Thus, in order to define $!\mathcal{A}(u)$ from the sets $\mathcal{A}(a_i)$, we generate an endomorphism of $a_i$ for every $i \in [n]$, using the following steps.

**Definition 6.1.** For $\sigma \in \mathfrak{S}_n$ and $i \in [n]$, let $o(\sigma, i)$ be the smallest strictly positive integer such that $\sigma^{o(\sigma, i)}(i) = i$. Equivalently, $o(\sigma, i)$ is the length of the cycle containing $i$ in the disjoint cycle decomposition of the permutation $\sigma$. If there is no ambiguity on the permutation, we just write $o(i)$ for $o(\sigma, i)$.

**Lemma 6.2.** Let $n$ be in $\mathbb{N}$ and $\sigma, \tau, \phi$ be permutations in $\mathfrak{S}_n$. If $\sigma = \varphi^{-1}\tau\varphi$, then for all $i \in [n]$, $o(\sigma, i) = o(\tau, \varphi(i))$.

*Proof.* We have $\sigma^{o(\tau, \varphi(i))}(i) = \varphi^{-1}\tau^{o(\tau, \varphi(i))}\varphi(i) = \varphi^{-1}\varphi(i) = i$. Assume that there exists $0 < j < o(\tau, \varphi(i))$ such that $\sigma^j(i) = i$, then $\tau^j\varphi(i) = \varphi\sigma^j(i) = \varphi(i)$ which contradicts the minimality of $o(\tau, \varphi(i))$. $\square$

**Definition 6.3.** For a sequence $u = \langle a_1, \dots, a_n \rangle$ in $\Sigma\mathbb{A}$ and a morphism $\alpha \in \Sigma\mathbb{A}(u, u)$, we define for each $i \in [n]$, an endomorphism $\text{loop}_i^\alpha : a_i \to a_i$ as the composite

$$ a_i \xrightarrow{\alpha_i} a_{\sigma(i)} \xrightarrow{\alpha_{\sigma(i)}} a_{\sigma^2(i)} \dots \xrightarrow{\alpha_{\sigma^{o(i)-1}(i)}} a_i $$

**Definition 6.4.** For a Boolean kit $(\mathbb{A}, \mathcal{A})$, $! (\mathbb{A}, \mathcal{A})$ is defined as $(\Sigma\mathbb{A}, (\mathcal{A}^{\Sigma})^{\perp})$, where for an object $u = \langle a_1, \dots, a_n \rangle \in \Sigma\mathbb{A}$, $\mathcal{A}^{\Sigma}(u)$ is given by:

$$ \{ H \le \text{End}_\mathbb{A}(u) \mid \forall \alpha \in H. \forall i \in [n], \text{loop}_i^\alpha \in \mathcal{A}(a_i) \} $$
Since the kit $\mathcal{A}^{\Sigma}$ is not Boolean in general, the closure under double orthogonality ensures that $!\mathcal{A} = (\mathcal{A}^{\Sigma})^{\perp\perp}$ is indeed a Boolean kit. We show that the operation $(\mathcal{A}, \mathcal{A}) \mapsto !\mathcal{(A}, \mathcal{A})$ extends to a pseudo-comonad on **SProf**. The proof is a technical but straightforward verification involving the characterisation described in Lemma 4.9.

**Proposition 6.5.** For Boolean kits $(\mathcal{A}, \mathcal{A})$ and $(\mathbb{B}, \mathcal{B})$ and $P: (\mathcal{A}, \mathcal{A}) \to (\mathbb{B}, \mathcal{B})$ a stabilized profunctor, the profunctor $\Sigma P: \Sigma\mathcal{A} \to \Sigma\mathbb{B}$ is a stabilized profunctor $!\mathcal{(A}, \mathcal{A}) \to !\mathbb{(B}, \mathcal{B})$.

*Proof.* Recall that for objects $u = \langle a_1, \dots, a_n \rangle \in \Sigma\mathcal{A}$ and $v = \langle b_1, \dots, b_n \rangle \in \Sigma\mathbb{B}$, the profunctor $\Sigma P: \Sigma\mathcal{A} \to \Sigma\mathbb{B}$ is given by:

$$ \Sigma P(v, u) = \begin{cases} \coprod_{\varphi \in \mathfrak{S}_n} \coprod_{j \in [m]} P(b_j, a_{\varphi(j)}), & \text{if } n = m \\ \emptyset, & \text{otherwise} \end{cases} $$

with the following functorial action: for an element $p = (\varphi, \langle p_j \rangle_{j \in [m]}) \in \Sigma P(v, u)$ and morphisms $\alpha = (\sigma, \langle \alpha_i \rangle_{i \in [n]}) : u \to u'$ and $\beta = (\tau, \langle \beta_j \rangle_{j \in [m]}) : v' \to v$,

$$ \alpha \cdot p \cdot \beta = (\sigma \circ \varphi \circ \tau, \langle \alpha_{\varphi(\tau(j))} \cdot p_{\tau(j)} \cdot \beta_j \rangle_{j \in [m]}). $$

Assume that there exists morphisms $\alpha = (\sigma, (\alpha_i)_{i \in [n]}) \in \mathrm{Endo}(u)$, $\beta = (\tau, (\beta_i)_{i \in [n]}) \in \mathrm{Endo}(v)$, and $p = (\varphi, (p_i)_{i \in [n]})$ be in $\Sigma P(v, u)$ such that $\alpha \cdot p \cdot \beta = p$, i.e.

$$ \sigma \circ \varphi \circ \tau = \varphi $$

and for all $i \in [n]$,

$$ \alpha_{\varphi(\tau(i))} \cdot p_{\tau(i)} \cdot \beta_i = p_i. $$

We first show that it implies that for all $i \in [n]$, $\mathrm{loop}_{\varphi(i)}^{\alpha} \cdot p_i \cdot \mathrm{loop}_{i}^{\beta} = p_i$. By Lemma 6.2, we have:

$$ \begin{aligned} \mathrm{loop}_{\varphi(i)}^{\alpha} \cdot p_i \cdot \mathrm{loop}_{i}^{g} &= \alpha_{\sigma^{o}(\sigma, \varphi)-1}(\varphi(i)) \cdots \alpha_{\sigma\varphi(i)}\alpha_{\varphi(i)} \cdot p_i \cdot \beta_{\tau^{o}(\tau, i)-1}(i) \cdots \beta_{\tau(i)} \cdot \beta_i \\ &= \alpha_{\sigma^{o}(\tau, i)-1}(\varphi(i)) \cdots \alpha_{\sigma\varphi(i)}\alpha_{\varphi(i)} \cdot p_i \cdot \beta_{\tau^{o}(\tau, i)-1}(i) \cdots \beta_{\tau(i)} \cdot \beta_i \end{aligned} $$

Note that since $\tau^{o(\tau, i)}(i) = i$, $\tau^{o(\tau, i)-1}(i) = \tau^{-1}(i)$ we have $\alpha_{\varphi(i)} \cdot p_i \cdot \beta_{\tau^{o(\tau, i)-1}(i)} = \alpha_{\varphi\tau(\tau^{-1}(i))} \cdot p_{\tau(\tau^{-1}(i))} \cdot \beta_{\tau^{-1}(i)} = p_{\tau^{-1}(i)}$. Repeating this process, we obtain the desired result. We now show that the following two implications hold:

$$ \alpha \in \bigcup !\mathcal{A}(u) \Rightarrow \beta \in \bigcup !\mathcal{B}(v) \quad \text{and} \quad \beta \in \bigcup !\mathcal{B}^{\perp}(v) \Rightarrow \alpha \in \bigcup !\mathcal{A}^{\perp}(u). $$

* Assume that $\alpha \in \bigcup !\mathcal{A}(u)$. By Lemma 4.9, it is equivalent to the following formula:

$$ \forall m \in \mathbb{N}, \alpha^m = \mathrm{id} \lor (\exists k \in \mathbb{N}, \alpha^{mk} \neq \mathrm{id} \land (\forall i \in [n], \mathrm{loop}_{a_i}^{\alpha^{mk}} \in \mathcal{A}(a_i))). $$

Let $m \in \mathbb{N}$ be such that $\beta^m \neq \mathrm{id}$, if $\alpha^m = \mathrm{id}$, then $\sigma^m = \mathrm{id}$ and for all $i \in [n]$, $\alpha_i^m = \mathrm{id} \in \mathcal{A}(a_i)$. It implies that $\tau^m = \mathrm{id}$ since $\sigma^m \circ \varphi \circ \tau^m = \varphi$ and for all $i \in [n]$, $\mathrm{loop}_i^{\beta^m} = \beta_i^m \in \mathcal{B}(b_i)$ since $\alpha_i \cdot p_i \cdot \beta_i = p_i$ and $P$ is a stabilized profunctor. Hence $\beta \in !\mathcal{B}(v)$ by Lemma 4.6.1.s If $\alpha^m \neq \mathrm{id}$, then there exists $k \in \mathbb{N}$ such that $\alpha^{mk} \neq \mathrm{id}$ and for all $i \in [n]$, $\mathrm{loop}_i^{\alpha^{mk}} \in \mathcal{A}(a_i)$. Since $P$ is a stabilized profunctor and $\mathrm{loop}_i^{\alpha^{mk}} \cdot p_i \cdot \mathrm{loop}_i^{\beta^{mk}} = p_i$, we have $\mathrm{loop}_i^{\beta^{mk}} \in \mathcal{B}(b_i)$ for all $i \in [n]$. It remains to show that $\beta^{mk} \neq \mathrm{id}$. If $\beta^{mk} = \mathrm{id}$, then $\tau^{mk} = \mathrm{id}$ and $\mathrm{loop}_i^{\beta^{mk}} = \beta_i^{mk} = \mathrm{id} \in \mathcal{B}^{\perp}(b_i)$ for all $i$. It implies that $\sigma^{mk} = \mathrm{id}$ and $\mathrm{loop}_i^{\alpha^{mk}} = \alpha_i^{mk} \in \mathcal{A}^{\perp}(a_i)$ for all $i \in [n]$ as $P$ is a stabilized profunctor. Hence, we must have $\alpha_i^{mk} = \mathrm{id}$ for all $i$ which implies that $\alpha^{mk} = \mathrm{id}$ since $\alpha_i^{mk} \in \mathcal{A}(a_i)$ by assumption.
* Assume that $\beta \in \bigcup!\mathcal{B}^{\perp}(v)$ i.e. for all $m \in \mathbb{N}$, if for all $i \in [n]$, $\mathrm{loop}_i^{\beta^m} \in \mathcal{B}(b_i)$ then $\beta^m = \mathrm{id}$. Assume that there exists $m \in \mathbb{N}$ such that for all $i \in [n]$, $\mathrm{loop}_i^{\alpha^m} \in \mathcal{A}(a_i)$. Since $\mathrm{loop}_{\varphi(i)}^{\alpha^m} \cdot p_i \cdot \mathrm{loop}_i^{\beta^m} = p_i$ for all $i \in [n]$ and $P$ is a stabilized profunctor, we have $\mathrm{loop}_i^{\beta^m} \in \mathcal{B}(b_i)$ for all $i \in [n]$ which implies that $\beta^m = \mathrm{id}$. Hence, $\tau^m = \mathrm{id}$ and for all $i \in [n]$, $\mathrm{loop}_i^{\beta^m} = \beta_i^m = \mathrm{id} \in \mathcal{B}^{\perp}(b_i)$ which entails that $\sigma^m = \mathrm{id}$ and $\mathrm{loop}_i^{\alpha^m} = \alpha_i^m \in \mathcal{A}^{\perp}(a_i)$ since $P$ is a stabilized profunctor. We conclude that $\alpha_i^m = \mathrm{id}$ for all $i \in [n]$ so that $\alpha^m = \mathrm{id}$ as desired. $\square$

As with the symmetric monoidal structure, the many coherence axioms required for a pseudo-comonad are immediately verified given the situation in **Prof**. All that is needed is that components of the counit and comultiplication, given above, are stabilized profunctors.

**Lemma 6.6.** For a Boolean kit $\mathcal{A} = (\mathcal{A}, \mathcal{A})$, the profunctor $\mathrm{der}_{\mathcal{A}} : \Sigma\mathcal{A} \dashrightarrow \mathcal{A}$ is a stabilized profunctor $!\mathcal{A} \dashrightarrow \mathcal{A}$.

*Proof.* This follows directly from observing that for a sequence $\langle a \rangle$ of length one in $\Sigma\mathcal{A}$,

$$ !\mathcal{A}(\langle a \rangle) = \{(\mathrm{id}, \langle \alpha \rangle) \mid \alpha \in \mathcal{A}(a)\} \cong \mathcal{A}(a). \quad \square $$

The next lemma is another technical verification based on the characterisation of Lemma 4.9.

**Lemma 6.7.** For a Boolean kit $(\mathcal{A}, \mathcal{A})$ and a sequence $\langle u_1, \dots, u_n \rangle \in \Sigma\Sigma\mathcal{A}$, there is a mapping

$$ \overline{(-)} : \mathrm{Endo}(\langle u_1, \dots, u_n \rangle) \to \mathrm{Endo}(u_1 \otimes \dots \otimes u_n) $$

such that for $\beta \in \mathrm{Endo}(\langle u_1, \dots, u_n \rangle)$, we have:

$$ \beta \in \bigcup!!\mathcal{A}(\langle u_1, \dots, u_n \rangle) \Leftrightarrow \bar{\beta} \in \bigcup!\mathcal{A}(u_1 \otimes \dots \otimes u_n) \quad \text{and} $$

$$ \beta \in \bigcup(!!\mathcal{A})^{\perp}(\langle u_1, \dots, u_n \rangle) \Leftrightarrow \bar{\beta} \in \bigcup(!\mathcal{A})^{\perp}(u_1 \otimes \dots \otimes u_n) $$

*Proof.* Let $\beta = (\tau, \langle \beta_i \rangle_{i \in [n]})$ be in $\mathrm{Endo}(\langle u_1, \dots, u_n \rangle)$ and let $n_i$ be the length of the sequence $u_i = \langle a_1^i, \dots, a_{n_i}^i \rangle$ for $1 \le i \le n$ and define $m$ to be $\sum_{i \in [n]} n_i$. For each $i$, $\beta_i$ consists of a permutation $\phi_i : [n_i] \to [n_i]$ and an $n_i$-tuple of morphisms $\langle \delta_j^i : a_j^i \to a_{\phi_i(j)}^{\tau(i)} \rangle_{j \in [n_i]}$ where $u_i = \langle a_1^i, \dots, a_{n_i}^i \rangle$. Define $\bar{\beta} = (\bar{\tau}, \langle \bar{\beta}_j \rangle_{j \in [m]}) \in \mathrm{Endo}(u_1 \otimes \dots \otimes u_n)$ as follows: the permutation $\bar{\tau} : [m] \to [m]$ is defined by:

$$ \bar{\tau} : k \mapsto \phi_{l+1}(k - \sum_{i=1}^{l} n_i) + \sum_{i=1}^{\tau(l+1)-1} n_i \quad \text{if} \quad \sum_{i=1}^{l} n_i < k \le \sum_{i=1}^{l+1} n_i $$

and for $1 \le k \le m$, we define $\bar{\beta}_k : a_k \to a_{\bar{\tau}(k)}$ as $\bar{\beta}_k := \delta_j^i$ where $i := l$ and $j := k - \sum_{i=1}^l n_i$ if $\sum_{i=1}^l n_i < k \le \sum_{i=1}^{l+1} n_i$. The idea is that if $\sum_{i=1}^l n_i < k \le \sum_{i=1}^{l+1} n_i$, then $k$ is in the subsequence $u_{l+1}$.

Note that for $a_j^i$ in $u_1 \otimes \dots \otimes u_n$, we have $\mathrm{loop}_{a_j^i}^{\bar{\beta}} = \mathrm{loop}_{u_i}^{\beta}$, therefore $\beta$ is in $\bigcup \mathcal{A}^{\Sigma\Sigma}(\langle u_1, \dots, u_n \rangle)$ if and only if $\bar{\beta}$ is in $\bigcup \mathcal{A}^{\Sigma}(u_1 \otimes \dots \otimes u_n)$. Since we further have
$\overline{\beta}^n = (\bar{\beta})^n$, we have $\beta \in \bigcup (!\mathcal{A})^{\perp} (\langle u_1, \dots, u_n \rangle)$ if an only if $\bar{\beta} \in \bigcup (!\mathcal{A})^{\perp} (u_1 \otimes \cdots \otimes u_n)$. It also implies that the following formulae are also equivalent:

$$ \forall n \in \mathbb{N}, \beta^n = \mathrm{id} \lor (\exists m \in \mathbb{N}, \beta^{nm} \neq \mathrm{id} \land \beta^{nm} \in \bigcup \mathcal{A}^{\Sigma\Sigma}(\langle u_1, \dots, u_n \rangle)) $$

$$ \forall n \in \mathbb{N}, \bar{\beta}^n = \mathrm{id} \lor (\exists m \in \mathbb{N}, \bar{\beta}^{nm} \neq \mathrm{id} \land \bar{\beta}^{nm} \in \bigcup \mathcal{A}^{\Sigma}(u_1 \otimes \cdots \otimes u_n)) $$

which implies that $\beta \in \bigcup !\mathcal{A}(\langle u_1, \dots, u_n \rangle)$ if an only if $\bar{\beta} \in \bigcup !\mathcal{A}(u_1 \otimes \cdots \otimes u_n)$ by Definition 4.8. $\square$

**Corollary 6.8.** For a Boolean kit $\mathcal{A} = (\mathcal{A}, \mathcal{A})$, the profunctor $\mathrm{dig}_{\mathcal{A}} : \Sigma\mathcal{A} \dashrightarrow \Sigma\Sigma\mathcal{A}$ is a stabilized profunctor $!\mathcal{A} \dashrightarrow !\mathcal{A}$.

*Proof.* Let $\gamma : u_1 \otimes \cdots \otimes u_n \to v$ be in $\mathrm{dig}_{\mathcal{A}}(\langle u_1, \dots, u_n \rangle, v)$, it is of the form $(\rho, \langle \gamma_k \rangle_{k \in [m]})$ where $\rho : [m] \xrightarrow{\sim} [m]$ and $\gamma_k : (u_1 \otimes \cdots \otimes u_n)_k \to v_{\rho(k)}$ for $1 \le k \le m$. Assume that there exists $\alpha = (\sigma, \langle \alpha_k \rangle_{k \in [m]}) \in \mathrm{Endo}(v)$ and $\beta = (\tau, \langle \beta_i \rangle_{i \in [m]}) \in \mathrm{Endo}(\langle u_1, \dots, u_n \rangle)$ such that $\alpha \cdot \gamma \cdot \beta = \gamma$. The morphism $\bar{\beta} : u_1 \otimes \cdots \otimes u_n \to u_1 \otimes \cdots \otimes u_n$ defined in Lemma 6.8 verifies $\gamma \cdot \beta = \gamma \circ \bar{\beta}$ which implies that $\alpha \cdot \gamma \cdot \beta = \gamma$ is equivalent to $\alpha \circ \gamma \circ \bar{\beta} = \gamma$ i.e.

$$ \sigma \rho \bar{\tau} = \rho \quad \text{and} \quad \alpha_{\rho \bar{\tau}(k)} \circ \gamma_{\bar{\tau}(k)} \circ \bar{\beta}_k = \gamma_k \quad \text{for all } 1 \le k \le m. $$

* Assume that $\alpha$ is in $\bigcup !\mathcal{A}(v)$, then $\bar{\beta}$ is in $\bigcup !\mathcal{A}(u_1 \otimes \cdots \otimes u_n)$ by closure under conjugation, which implies that $\beta$ is in $\bigcup !\mathcal{A}(\langle u_1, \dots, u_n \rangle)$ by Lemma 6.8.

* Assume that $\beta$ is in $\bigcup (!\mathcal{A})^{\perp}(\langle u_1, \dots, u_n \rangle)$, then $\bar{\beta}$ is in $\bigcup (!\mathcal{A})^{\perp}(u_1 \otimes \cdots \otimes u_n)$ by Lemma 6.8 which implies that $\alpha$ is in $\bigcup (!\mathcal{A})^{\perp}(v)$ by closure under conjugation. $\square$

**Proposition 6.9.** The pseudo-functor $! : \mathbf{SProf} \to \mathbf{SProf}$ extends to a pseudo-comonad.

As usual for orthogonality models of linear logic, the construction $? (\mathcal{A}, \mathcal{A}) := (\Sigma\mathcal{A}, (!\mathcal{A})^{\perp})$ induces a pseudo-monad structure on $\mathbf{SProf}$ that interprets the “why not” modality of linear logic. Note that, unlike in **Prof**, the connectives ! and ? are distinguished.

The coKleisli bicategory $\mathbf{SProf}_!$ is denoted $\mathbf{SEsp}$, and its morphisms are called *stable species of structures*. Besides the connection to stabilized profunctors, this choice of terminology is justified by their extensional characterisation as stable functors, which we provide in the second part of this paper.

## 6.2. Cartesian closed structure.
In this section, we show that the cartesian closed structure of $\mathbf{Esp} = \mathbf{Prof}_{\Sigma}$, first outlined in [FGHW08], extends to $\mathbf{SEsp}$.

The coKleisli bicategory $\mathbf{SProf}_!$ has binary products inherited from the linear category $\mathbf{SProf}$, i.e. given by the $\&$ construction of Sec. 5.1, and terminal object $(0, \emptyset)$. From here the path to cartesian closure is relatively standard, though not immediate. The structure is derived from the monoidal closed structure in $\mathbf{SProf}$ via a fundamental property of ! often referred to as the *Seely equivalence*:

$$ ! (\underline{\mathcal{A}} \& \underline{\mathcal{B}}) \simeq ! \underline{\mathcal{A}} \otimes ! \underline{\mathcal{B}}. $$

This property is derived from an adjoint equivalence

$$ \Sigma (\mathcal{A} \& \mathcal{B}) \xrightarrow{S_{\mathcal{A}, \mathcal{B}}} \Sigma \mathcal{A} \otimes \Sigma \mathcal{B} $$

in the bicategory **Prof**, which extends to $\mathbf{SProf}$.
**Lemma 6.10.** [FGHW08] For categories $\mathcal{A}$ and $\mathcal{B}$, consider the functor $\mathcal{A} \& \mathcal{B} \to \Sigma\mathcal{A} \otimes \Sigma\mathcal{B}$ mapping $(1, a)$ to $(\langle a \rangle, \diamondsuit)$ and $(2, b)$ to $(\langle \diamondsuit \rangle, \langle b \rangle)$, by the universal property of the completion $\Sigma$ it induces a functor $\Sigma(\mathcal{A} \& \mathcal{B}) \to \Sigma\mathcal{A} \otimes \Sigma\mathcal{B}$ that we denote by $S_{\mathcal{A},\mathcal{B}}$. We use the same notation as in [FGHW08] and write $(w.1, w.2)$ for the image of $w \in \Sigma(\mathcal{A} \& \mathcal{B})$ by $S_{\mathcal{A},\mathcal{B}}$. Let $T_{\mathcal{A},\mathcal{B}} : \Sigma\mathcal{A} \otimes \Sigma\mathcal{B} \to \Sigma(\mathcal{A} \& \mathcal{B})$ be the functor defined by

$$ (u, v) \mapsto (\Sigma\mathrm{inj}_1 u) \otimes (\Sigma\mathrm{inj}_2 v). $$

The functors $T_{\mathcal{A},\mathcal{B}}$ and $S_{\mathcal{A},\mathcal{B}}$ form an equivalence of categories $\Sigma(\mathcal{A} \& \mathcal{B}) \simeq \Sigma\mathcal{A} \otimes \Sigma\mathcal{B}$. We also have $\Sigma\mathbf{0} \simeq \mathbf{1}$.

**Lemma 6.11.** For Boolean kits $\mathcal{A} = (\mathcal{A}, \mathcal{A})$ and $\mathcal{A} = (\mathcal{A}, \mathcal{A})$, the mapping $(\alpha, \beta) \mapsto \alpha \otimes \beta$ induces an inclusion

$$ \mathcal{A}^{\Sigma}(u) \times \mathcal{B}^{\Sigma}(v) \subseteq (\mathcal{A} \& \mathcal{B})^{\Sigma}(u \otimes v) $$

*Proof.* The inclusion follows from the following observation: for $a \in \mathcal{A}$, $\mathrm{loop}^{\alpha \otimes \beta}_{(1,a)} = (1, \mathrm{loop}^{\alpha}_{a})$ and for $b \in \mathcal{B}$, $\mathrm{loop}^{\alpha \otimes \beta}_{(2,b)} = (2, \mathrm{loop}^{\beta}_{b})$. $\square$

**Lemma 6.12.** For Boolean kits $\mathcal{A} = (\mathcal{A}, \mathcal{A})$ and $\mathcal{B} = (\mathcal{B}, \mathcal{B})$, the Seely profunctors $S_{\mathcal{A},\mathcal{B}}$ and $T_{\mathcal{A},\mathcal{B}}$ are stabilized profunctors, so that there is an adjoint equivalence $! (\mathcal{A} \& \mathcal{B}) \simeq ! \mathcal{A} \otimes ! \mathcal{B}$ in $\mathbf{SProf}$. We also have $! \mathbf{0} \simeq \mathbf{1}$.

*Proof.* We show that for $(\alpha, \beta) \in (\mathrm{Endo}(u) \times \mathrm{Endo}(v))$, the mapping $(\alpha, \beta) \mapsto \alpha \otimes \beta$ induces an inclusion

$$ !\mathcal{A}(u) \times !\mathcal{B}(v) \hookrightarrow !\left(\mathcal{A} \& \mathcal{B}\right)(u \otimes v). $$

Assume that $(\alpha, \beta)$ is in $!\mathcal{A}(u) \times !\mathcal{B}(v)$ and that there exists $n \in \mathbb{N}$ such that $(\alpha \otimes \beta)^n \neq \mathrm{id}$. It implies that $(\alpha, \beta)^n \neq (\mathrm{id}, \mathrm{id})$, we suppose without loss of generality that $\alpha^n \neq \mathrm{id}$. Since $\alpha$ is in $!\mathcal{A}(u)$, there exists $m \in \mathbb{N}$ such that $\alpha^{nm} \neq \mathrm{id}$ and $\alpha^{nm} \in \mathcal{A}^{\Sigma}(u)$. If $\beta^{nm} = \mathrm{id}$ then $\beta^{nm} \in \mathcal{B}^{\Sigma}(v)$ so that $(\alpha, \beta)^{nm} \in \mathcal{A}^{\Sigma}(u) \times \mathcal{B}^{\Sigma}(v)$ which implies that $(\alpha \otimes \beta)^{nm} \in (\mathcal{A} \& \mathcal{B})^{\Sigma}(u \otimes v)$ by Lemma 6.11 and $\alpha^{nm} \neq \mathrm{id}$ entails that $(\alpha \otimes \beta)^{nm} \neq \mathrm{id}$.

If $\beta^{nm} \neq \mathrm{id}$ then since $\beta^{nm} \in !\mathcal{B}(v)$, there exists $l \in \mathbb{N}$ such that $\beta^{nml} \neq \mathrm{id}$ and $\beta^{nml} \in \mathcal{B}^{\Sigma}(v)$. Since $\mathcal{A}^{\Sigma}(u)$ is closed under powers, $\alpha^{nml}$ is in $\mathcal{A}^{\Sigma}(u)$ as well. Hence, by Lemma 6.11, $(\alpha \otimes \beta)^{nml} \in (\mathcal{A} \& \mathcal{B})^{\Sigma}(u \otimes v)$ and $\beta^{nml} \neq \mathrm{id}$ implies $(\alpha \otimes \beta)^{nml} \neq \mathrm{id}$. Hence, $(\alpha \otimes \beta)$ is in $!\left(\mathcal{A} \& \mathcal{B}\right)(u \otimes v)$ as desired.

We now obtain the desired inclusion.

$$ (!\mathcal{A} \otimes !\mathcal{B})(u, v) = (!\mathcal{A}(u) \times !\mathcal{B}(v))^{\perp \perp} \hookrightarrow (!\mathcal{A} \& \mathcal{B})^{\perp \perp}(u \otimes v) = (!\mathcal{A} \& \mathcal{B})(u \otimes v). $$

We show that for $\gamma \in \mathrm{Endo}(w)$, the mapping $\gamma \mapsto (\gamma.1, \gamma.2)$ induces an inclusion

$$ !\left(\mathcal{A} \& \mathcal{B}\right)(w) \hookrightarrow !\left(\mathcal{A} \otimes !\mathcal{B}\right)(w.1, w.2). $$

To do so, we show that $(\mathcal{A} \& \mathcal{B})^{\Sigma}(w) \hookrightarrow !\mathcal{A}(w.1) \times !\mathcal{B}(w.2)$ and the desired inclusion will follow by applying $(-)^{\perp \perp}$ on both sides. Assume that $\gamma$ is in $(\mathcal{A} \& \mathcal{B})^{\Sigma}(w)$, then since for elements $a$ in $w.1$ and $b$ in $w.2$

$$ \mathrm{loop}^{\gamma}_{(1,a)} = (1, \mathrm{loop}^{\gamma.1}_{a}) \quad \text{and} \quad \mathrm{loop}^{\gamma}_{(2,b)} = (2, \mathrm{loop}^{\gamma.2}_{b}) $$

we have $(\gamma.1, \gamma.2) \in (\mathcal{A}^{\Sigma}(w.1) \times \mathcal{B}^{\Sigma}(w.2)) \subseteq (!\mathcal{A}(w.1) \times !\mathcal{B}(w.2))$. $\square$
For Boolean kits $(\mathcal{A}, \mathcal{A})$ and $(\mathcal{B}, \mathcal{B})$, the internal hom $\underline{\mathcal{A}} \to \mathcal{B} = (\underline{\mathcal{A}} \otimes \mathcal{B}^{\perp})^{\perp}$ in **SProf** comes equipped with a linear evaluation morphism $\mathrm{ev}_{\mathcal{A},\mathcal{B}} : \underline{\mathcal{A}} \otimes (\underline{\mathcal{A}} \to \mathcal{B}) \dashrightarrow \mathcal{B}$. We define the function space in **SProf**! as

$$ (\mathcal{A}, \mathcal{A}) \Rightarrow (\mathcal{B}, \mathcal{B}) = ! (\mathcal{A}, \mathcal{A}) \to (\mathcal{B}, \mathcal{B}) $$

and the cartesian evaluation $\mathrm{Ev}_{\mathcal{A},\mathcal{B}} : (\Sigma(\mathcal{A} \Rightarrow \mathcal{B}) \& \mathcal{A}) \dashrightarrow \mathcal{B}$ as the morphism

$$ \mathrm{ev}_{\Sigma\mathcal{A},\mathcal{B}} \circ (\mathrm{der}_{\mathcal{A}\Rightarrow\mathcal{B}} \otimes \mathrm{id}) \circ S_{\mathcal{A}\Rightarrow\mathcal{B},\mathcal{A}} $$

As a composite of stabilized profunctors, $\mathrm{Ev}_{\mathcal{A},\mathcal{B}}$ is in **SProf**!($\underline{\mathcal{A}} \Rightarrow \mathcal{B}$) & $\underline{\mathcal{A}}, \mathcal{B}$). For a stable species $P$ in **SProf**!($\underline{\mathcal{A}} \& \mathcal{B}, \mathcal{C}$), its *currying* $\Lambda(P) \in \mathrm{SProf}!(\underline{\mathcal{A}}, \mathcal{B} \Rightarrow \mathcal{C})$ is given by $\lambda(P \circ T_{\mathcal{A},\mathcal{B}})$, where

$$ \lambda : \mathrm{SProf}!(\underline{\mathcal{A}} \otimes !\mathcal{B}, \mathcal{C}) \to \mathrm{SProf}!(\underline{\mathcal{A}}, !\mathcal{B} \to \mathcal{C}) $$

is provided by the monoidal closed structure on **SProf**.

**Theorem 6.13.** *The bicategory **SEsp** is cartesian closed.*

*Proof.* The adjoint equivalence

<figure><img src="image_4.png" /></figure>

is obtained directly from the Seely adjoint equivalence. $\square$

**6.3. Differential structure.** To a combinatorial species $F : \mathbf{Bij} \to \mathbf{Set}$, one can associate an exponential generating series of the form $x \mapsto \sum_{n \ge 0} f_n \frac{x^n}{n!}$. Here, $f_n$ is identified with the cardinality of the set $F([n])$, interpreted as the number of $F$-structures of size $n$. This formal power series has a derivative:

$$ x \mapsto \sum_{n \ge 1} f_n n \frac{x^{n-1}}{n!} = \sum_{m \ge 0} f_{m+1} \frac{x^m}{m!} $$

and the corresponding species is the functor **Bij** $\to \mathbf{Set}$ : $[n] \mapsto F([n+1])$.

This combinatorial notion extends to the wider universe of generalized species [Fio05]. A generalized species $F : \Sigma\mathcal{A} \dashrightarrow \mathcal{B}$ has a differential **DF** : $!\mathcal{A} \otimes \mathcal{A} \dashrightarrow \mathcal{B}$ with action

$$ (b, (u, a)) \mapsto F(b, u \otimes \langle a \rangle), $$

which coincides with the above construction when $\mathcal{A} = \mathcal{B} = 1$.

The combinatorial notion of differentiation has a logical counterpart in the framework of *differential linear logic* put forward by Ehrhard et al. [ER03, Ehr18], which extends linear logic with operators for differentiation. The bicategory **Prof** provides a model for differential linear logic, in which logical derivatives are formally assigned a combinatorial interpretation [Fio05].

The differential operators of **Prof** extend to **SProf**, which we show is also a model for differential linear logic. Indeed, given a model of linear logic with biproducts, the structure required to model differential operators is relatively minimal [Fio07]. The fact that **SProf** is a model for differential linear logic follows from the forgetful functor to **Prof**, which ensures that coherence axioms are satisfied, together with the following direct observation:
**Lemma 6.14.** For a kit $\mathcal{A} = (\mathcal{A}, \mathcal{A})$, the profunctor $\overline{\mathrm{der}}_{\mathcal{A}} : \mathcal{A} \dashrightarrow \Sigma\mathcal{A}$ given by $(u, a) \dashrightarrow \Sigma\mathcal{A}(u, \langle a \rangle)$ is a stabilized profunctor $\mathcal{A} \dashrightarrow !\mathcal{A}$.

We finally note that, although species $\mathbf{Bij} \to \mathbf{Set}$ can be differentiated, they do not support an adequate notion of integration as needed for instance in the resolution of differential equations [LV88]. It is known however that “L-species”, which correspond to N-indexed families of sets without any symmetric group actions, enjoy uniqueness and existence theorems for solutions of differential equations [BLL98]. As L-species correspond to our stable species $!\mathbf{1} \dashrightarrow \mathbf{1}$, the bicategory $\mathbf{SEsp}$ appears as a candidate framework for the study of formal differential equations, providing a bridge to similar investigations on the logical side [Ker18, KL19].

## EXTENSIONAL THEORY: LINEAR AND STABLE FUNCTORS

In the rest of the paper, we study the extensional aspects of stabilized profunctors and stable species. We will see, in Sections 8 and 9, that both stabilized profunctors and stable species can be characterized extensionally as functors between subcategories of presheaves, which one can view as generalized Scott domains. We give a biequivalence between the bicategory of stable species and a 2-category of stable functors, and as a corollary we obtain that the latter is cartesian closed.

### 7. CATEGORIES OF STABILIZED PRESHEAVES

First we describe and study these subcategories of presheaves, by considering presheaves that arise as global elements $1 \dashrightarrow (\mathcal{A}, \mathcal{A})$ in $\mathbf{SProf}$, which we call stabilized presheaves. For a kit $(\mathcal{A}, \mathcal{A})$, a presheaf $X : \mathcal{A}^{\circ} \to \mathbf{Set}$ defines a stabilized profunctor $\mathbf{1} \dashrightarrow (\mathcal{A}, \mathcal{A})$ if and only if, for all $a \in \mathcal{A}$, $x \in X(a)$, and $\alpha : a \to a$,

$$x \cdot \alpha = x \implies \alpha \in \bigcup \mathcal{A}(a).$$

This property is more succinctly expressed using the group-theoretic notion of stabilizer: for $a \in \mathcal{A}$ and $x \in X(a)$, we denote by $\mathrm{Stab}(x)$ the subgroup of $\mathrm{Endo}(a)$ consisting of those endomorphisms $\alpha$ such that $x \cdot \alpha = x$. We now define $(\mathcal{A})$-stabilized presheaves as those presheaves whose elements all have stabilizer in $\mathcal{A}$.

**Definition 7.1.** For a kit $(\mathcal{A}, \mathcal{A})$ we let $\mathcal{S}(\mathcal{A}, \mathcal{A})$ be the full subcategory of $\mathcal{P}(\mathcal{A})$ consisting of presheaves $X$ such that for every $a \in \mathcal{A}$ and $x \in X(a)$, $\mathrm{Stab}(x) \in \mathcal{A}(a)$; we call these stabilized presheaves.

When $\mathcal{A} = (\mathcal{A}, \mathcal{A})$ is a Boolean kit, there is an equivalence of categories $\mathbf{SProf}(\mathbf{1}, \mathcal{A}) \simeq \mathcal{S}(\mathcal{A})$. In this section, we focus on properties of the subcategory $\mathcal{S}(\mathcal{A})$ for an arbitrary kit $\mathcal{A}$. First we observe that for a groupoid $\mathcal{A}$, the operation sending a kit $\mathcal{A}$ to the category $\mathcal{S}(\mathcal{A}, \mathcal{A})$ has a right inverse.

**Lemma 7.2.** For a groupoid $\mathcal{A}$ and a full subcategory $\mathcal{S}$ of $\mathcal{P}(\mathcal{A})$, the family $\mathrm{Stab}(\mathcal{S})$ defined by

$$\mathrm{Stab}(\mathcal{S})(a) = \{G \mid \exists X \in \mathcal{S}, \exists x \in X(a), G = \mathrm{Stab}(x)\} \\ \text{is a kit on } \mathcal{A}. \text{ Additionally, } \mathrm{Stab}(\mathcal{S}(\mathcal{A}, \mathcal{A})) = (\mathcal{A}, \mathcal{A}) \text{ and } \mathcal{S} \subseteq \mathcal{S}(\mathcal{A}, \mathrm{Stab}(\mathcal{S})).$$
**7.1. Stabilized quotients of representables.** For an object $a$ of a groupoid $\mathbb{A}$, consider the representable presheaf $y(a) : \mathbb{A}^{\circ} \to \text{Set}$. For $a' \in \mathbb{A}$, every element $\gamma \in y(a)(a') = \mathbb{A}(a', a)$ has trivial stabilizer, since in a groupoid $\gamma \circ \alpha = \gamma$ implies $\alpha = \text{id}$. To generate stabilized presheaves, we consider representables *quotiented* by kit subgroups.

**Definition 7.3.** For an object $a$ of a groupoid $\mathbb{A}$ and $G \leqslant \text{End}(a)$, let $y(a|G) \in \mathcal{P}(\mathbb{A})$ be the quotient of $y(a)$ under $G$; that is, the colimit of the composite $G \to \mathbb{A} \hookrightarrow \mathcal{P}(\mathbb{A})$.

In elementary terms, the presheaf $y(a|G)$ maps an object $a'$ to the quotient of $y(a)(a') = \mathbb{A}(a', a)$ under the equivalence relation $\sim_G$ given by $\gamma' \sim_G \gamma$ if and only if $\gamma' \gamma^{-1} \in G$. For example, $y(a|\text{Triv}(a)) \cong y(a)$, and $y(a|\text{End}(a))(a')$ is a singleton when $a \cong a'$, and $\emptyset$ otherwise.

**Lemma 7.4.** For $(\mathbb{A}, \mathcal{A})$ a kit, $a \in \mathbb{A}$ and $G \in \mathcal{A}(a)$, $y(a|G) \in \mathcal{S}(\mathbb{A}, \mathcal{A})$.

*Proof sketch.* The stabilizer of an element $[\alpha]_{\sim_G} \in y(a|G)(a')$ is the conjugate subgroup $\alpha^{-1}G\alpha$, which is in $\mathcal{A}(a')$ since kits are closed under conjugation. $\square$

**7.2. Stabilized presheaves as coproduct completions.** We show that in fact $\mathcal{S}(\mathbb{A}, \mathcal{A})$ is equivalent to the free coproduct completion of the full subcategory of $\mathcal{P}(\mathbb{A})$ spanned by quotients of representables of the form $y(a|G)$, for $a \in \mathbb{A}$ and $G \in \mathcal{A}(a)$. The first step in showing this is to observe that $\mathcal{S}(\mathbb{A}, \mathcal{A})$ has all coproducts, calculated as in $\mathcal{P}(\mathbb{A})$. This holds because for presheaves $X$ and $Y$, the stabilizer of an element of $X + Y$ is equal to the stabilizer of the corresponding element in $X$ or $Y$.

Next, we show a representation theorem stating that every object of $\mathcal{S}(\mathbb{A}, \mathcal{A})$ can be obtained as a sum of quotients of representables of the form $y(a|G)$, with $a \in \mathbb{A}$ and $G \in \mathcal{A}(a)$.

**Lemma 7.5.** For a kit $(\mathbb{A}, \mathcal{A})$, using the axiom of choice, every presheaf $X \in \mathcal{S}(\mathbb{A}, \mathcal{A})$ has a representation

$$X \cong \coprod_{i \in I} y(a_i|G_i)$$

where each $a_i \in \mathbb{A}$ and $G_i \in \mathcal{A}(a_i)$.

*Proof.* Using the axiom of choice, we choose a representative $a_c \in \mathbb{A}$ for each connected component $c \in \pi_0(\mathbb{A})$. For each $x \in X(a)$, we denote by $o(x) := \{x \cdot \alpha \mid \alpha \in \mathbb{A}(a, a)\}$, the orbit of $x$. For $a \in \mathbb{A}$, we write $\text{Orbits}(X(a)) := \{o(x) \mid x \in X(a)\}$ for the set of orbits of $X(a)$. Using the axiom of choice again, we chose a representative $x_i$ for each orbit $i \in \text{Orbits}(X(a))$. We define the presheaf $Y$ as:

$$\coprod_{c \in \pi_0(\mathbb{A})} \coprod_{i \in \text{Orbits}(X(a_c))} y(a_c|\text{Stab}(x_i))$$

Let $f : Y \Rightarrow X$ be the natural transformation whose components $f_a$ are given by:

$$(c, i, [\alpha : a \to a_c]) \mapsto x_i \cdot \alpha$$

We first start by showing that $f_a$ is well-defined: assume that $[\alpha] = [\beta]$ i.e. $\alpha\beta^{-1}$ is in $\text{Stab}(x_i)$, then $x_i \cdot (\alpha\beta^{-1}) = x_i$ which implies that $x_i \cdot \alpha = x_i \cdot \beta$ as desired.

For surjectivity, let $x$ be in $X(a)$ and let $c$ be the connected component containing $a$ so there exists a morphism $\gamma : a_c \to a$. Let $x_i$ be the representative of the orbit $o(x \cdot h) \in \text{Orbits}(X(a_c))$ so there exists $\beta : a_c \to a_c$ such that $x \cdot \gamma = x_i \cdot \beta$. The element $(c, o(x \cdot \gamma), [\beta\gamma^{-1}])$ in $Y(a)$ is then a preimage of $x$ as $x_i \cdot \beta\gamma^{-1} = x$.
For injectivity, let $(c, i, [\alpha : a \to a_c])$ and $(d, j, [\beta : a \to a_d])$ be two elements of $Y(a)$ such that $x_i \cdot \alpha = x_j \cdot \beta$. Since $\beta\alpha^{-1} \in \mathbb{A}(a_c, a_d)$, $a_c$ and $a_d$ are in the same connected component which implies that $c = d$ and therefore $a_c = a_d$ since there is one representative chosen for each component. Hence, we have $x_i = x_j \cdot (\beta\alpha^{-1}) \in X(a_c)$ which implies that $x_i$ and $x_j$ are in the same orbit so $i = j$ and $x_i = x_j$ since there is one representative chosen for each orbit. We now have $x_i = x_j \cdot (\beta\alpha^{-1})$ which implies that $[\alpha] = [\beta]$.

Naturality of $f$ is immediate so we conclude that it is a natural isomorphism. $\square$

**Corollary 7.6.** For a kit $(\mathbb{A}, \mathcal{A})$, using the axiom of choice, every presheaf in $\mathcal{S}(\mathbb{A}, \mathcal{A})$ has a representation as a filtered colimit of finitely presentable presheaves of the form $\coprod_{i \in I} y(a_i|G_i)$ with the set $I$ finite and each group $G_i \in \mathcal{A}(a_i)$ is finitely generated for $i \in I$.

From this we derive the following:

**Proposition 7.7.** For $(\mathbb{A}, \mathcal{A})$ a kit, the category $\mathcal{S}(\mathbb{A}, \mathcal{A})$ is equivalent to the free coproduct completion of the full subcategory of $\mathcal{P}(\mathbb{A})$ spanned by the $y(a|G)$, for $a \in \mathbb{A}$ and $G \in \mathcal{A}(a)$.

*Proof sketch.* Write $\coprod_{\mathcal{A}}$ for this completion. Since $\mathcal{S}(\mathbb{A}, \mathcal{A})$ contains the $y(a|G)$ and has all coproducts there is a canonical functor $\coprod_{\mathcal{A}} \to \mathcal{S}(\mathbb{A}, \mathcal{A})$. It is full and faithful by a straightforward argument and essentially surjective on objects by Lemma 7.5. $\square$

**7.3. Presheaves and orthogonality.** In this section, we show that the duality enjoyed by the kits on a groupoid $\mathbb{A}$ through the $(-)^{\perp}$ construction translates to a duality between presheaves and co-presheaves over $\mathbb{A}$. Presheaves over $\mathbb{A}$ (equivalently profunctors $1 \dashrightarrow \mathbb{A}$) are thought of as modelling closed programs of type $\mathbb{A}$ and co-presheaves (or profunctors $\mathbb{A} \dashrightarrow 1$) provide a notion of program environment<fnref n="2" />. In this viewpoint, orthogonality provides a refined setting in which one explicitly controls the possible interactions between programs and environments. Here we ensure that the stabilizer groups on either side of the interaction have no elements in common but the identity.

**Definition 7.8.** For a groupoid $\mathbb{A}$, a presheaf $X : \mathbb{A}^{\circ} \to \mathbf{Set}$ and a co-presheaf $Y : \mathbb{A} \to \mathbf{Set}$, we say that $X$ and $Y$ are *orthogonal*, written $X \perp Y$, if the presheaf on $\mathbb{A}$ with object mapping $a \mapsto X(a) \times Y(a)$ and functorial action defined by

$$ (x, y) \cdot \alpha = (x \cdot \alpha, \alpha^{-1} \cdot y) $$

is free: all its elements have trivial stabilizer. Explicitly, a presheaf $Z \in \mathcal{P}(\mathbb{A})$ is free whenever, for all $\alpha, \beta : a' \to a$ in $\mathbb{A}$ and $z \in Z(a)$,

$$ z \cdot \alpha = z \cdot \beta \implies \alpha = \beta. $$

Orthogonality in this sense is the counterpart, in our model, of the orthogonality relations underlying a number of well-known models of classical linear logic [Gir86, Loa94, Ehr05, DE11]. All of these models were given a unified, axiomatic treatment based on *double-glueing* categories along hom-functors, in a framework developed by Hyland and Shalk [HS03]. The bicategorical version of this framework, which should encompass the model of this paper, has yet to be worked out.

<footnote n="2">²This duality has many alternative descriptions as proofs/counterproofs, Player/Opponent, etc.</footnote>
The following construction may then be performed on subcategories of presheaves: for any full subcategory $\mathcal{S}$ of $\mathcal{P}(\mathbb{A})$, the category $\mathcal{S}^{\perp}$ is the full subcategory of $\mathcal{P}(\mathbb{A}^{\circ})$ with objects

$$ \{Y : \mathbb{A} \to \mathbf{Set} \mid \forall X \in \mathcal{S}, X \perp Y\}. $$

The two notions of duality (on kits and full subcategories) are closely related. Let $\mathbf{FS}(\mathbb{A})$ be the (large) poset of full subcategories of $\mathcal{P}(\mathbb{A})$ under inclusion. As with kits, the orthogonality relation induces a Galois connection

$$ \mathbf{FS}(\mathbb{A})^{\circ} \xrightarrow{(-)^{\perp}} \mathbf{FS}(\mathbb{A}^{\circ}) \xleftarrow{\perp} (-)^{\perp} $$

whose fixed points are those $\mathcal{S}$ verifying $\mathcal{S}^{\perp\perp} = \mathcal{S}$. Thus we have two notions of duality, respectively intensional (based on subgroups) and extensional (based on presheaves). These are fundamentally connected via the equations

$$ \mathcal{S}(\mathbb{A}, \mathcal{A})^{\perp} = \mathcal{S}(\mathbb{A}^{\circ}, \mathcal{A}^{\perp}) \quad \text{and} \quad \mathrm{Stab}(\mathcal{S})^{\perp} = \mathrm{Stab}(\mathcal{S}^{\perp}) $$

from which we derive another characterization of Boolean kits as those kits $(\mathbb{A}, \mathcal{A})$ satisfying $\mathcal{S}(\mathbb{A}, \mathcal{A})^{\perp\perp} = \mathcal{S}(\mathbb{A}, \mathcal{A})$. Moreover, our earlier definition of stabilized profunctor (Definition 4.10) may be rephrased in extensional style:

**Lemma 7.9.** A profunctor $P : \mathbb{A} \dashrightarrow \mathbb{B}$ induces two functors $P^{\#} := \mathrm{Lan}_{\mathrm{y}_{\mathbb{A}}} P : \mathcal{P}(\mathbb{A}) \to \mathcal{P}(\mathbb{B})$ and $P_{\#} := (P^{\circ})^{\#} : \mathcal{P}(\mathbb{B}^{\circ}) \to \mathcal{P}(\mathbb{A}^{\circ})$. For Boolean kits $\mathbb{A} = (\mathbb{A}, \mathcal{A})$ and $\mathbb{B} = (\mathbb{B}, \mathcal{B})$, $P$ is a stabilized profunctor from $\mathbb{A}$ to $\mathbb{B}$ if and only if

$$ \begin{array}{ccc} \mathcal{P}(\mathbb{A}) & \xrightarrow{P^{\#}} & \mathcal{P}(\mathbb{B}) \\ \biguparrow & & \biguparrow \\ \mathcal{S}(\mathbb{A}) \dashrightarrow \mathcal{S}(\mathbb{B}) & \text{and} & \mathcal{S}(\mathbb{B}^{\star}) \dashrightarrow \mathcal{S}(\mathbb{A}^{\star}) \end{array} $$

That is, $P^{\#} : \mathcal{P}(\mathbb{A}) \to \mathcal{P}(\mathbb{B})$ restricts to a functor $\mathcal{S}(\mathbb{A}) \to \mathcal{S}(\mathbb{B})$ and $P_{\#} : \mathcal{P}(\mathbb{A}^{\circ}) \to \mathcal{P}(\mathbb{B}^{\circ})$ restricts to a functor $\mathcal{S}(\mathbb{B}^{\star}) \to \mathcal{S}(\mathbb{A}^{\star})$.

*Proof.*

(⇒) Assume that $P : \mathbb{A} \dashrightarrow \mathbb{B}$ is a stabilized profunctor. For $X \in \mathcal{S}(\mathbb{A})$ and $b \in \mathbb{B}$ we want to show that the stabilizer of every element in $P^{\#}X(b) = \int^{a \in \mathbb{A}} P(b, a) \times X(a)$ is in $\mathcal{B}(b)$. Let $t = p \underset{\mathbb{A}}{\boxtimes} x$ be in $P^{\#}X(b)$. For every $\beta : b \to b$ in $\mathrm{Stab}(t)$, we have $(p \cdot \beta) \underset{\mathbb{A}}{\boxtimes} x = (p \underset{\mathbb{A}}{\boxtimes} x) \cdot \beta = p \underset{\mathbb{A}}{\boxtimes} x$, i.e. there exists $\alpha : a \to a$ in $\mathbb{A}$ such that $\alpha \cdot p \cdot \beta = p$ and $x \cdot \alpha = x$. Since $X$ is in $\mathcal{S}(\mathbb{A})$, we must have $\alpha \in \bigcup \mathcal{A}(a)$ and since $P$ is a stabilized profunctor, we must also have $g \in \bigcup \mathcal{B}(b)$ as desired. One shows that $P_{\#}Y$ is in $\mathcal{S}(\mathbb{A}^{\perp})$ for $Y \in \mathcal{S}(\mathbb{B}^{\perp})$ analogously.

( ⇐ ) Assume that $P^{\#}(\mathcal{S}(\mathbb{A})) \hookrightarrow \mathcal{S}(\mathbb{B})$. Let $a \in \mathbb{A}$, $b \in \mathbb{B}$, $p \in P(b, a)$, $\alpha \in \mathbb{A}(a, a)$, and $\beta \in \mathbb{B}(b, b)$ be such that $\alpha \cdot p \cdot \beta = p$. Suppose that $\alpha \in \bigcup \mathcal{A}(a)$ and let $X = y(a|\langle \alpha \rangle) \in \mathcal{S}(\mathbb{A})$. We then have $P^{\#}(X) \in \mathcal{S}(\mathbb{B})$ by hypothesis. Hence, for the element $p \underset{\mathbb{A}}{\boxtimes} \langle \alpha \rangle = p \underset{\mathbb{A}}{\boxtimes} \langle \alpha \rangle \alpha = (\alpha \cdot p) \underset{\mathbb{A}}{\boxtimes} \langle \alpha \rangle$ in $P^{\#}X(b)$, it follows that $(p \underset{\mathbb{A}}{\boxtimes} \langle \alpha \rangle) \cdot \beta = (\alpha \cdot p \cdot \beta) \underset{\mathbb{A}}{\boxtimes} \langle \alpha \rangle = p \underset{\mathbb{A}}{\boxtimes} \langle \alpha \rangle$ which implies $\beta \in \bigcup \mathcal{B}(b)$ as desired.

Assuming $P_{\#}(\mathcal{S}(\mathbb{B}^{\perp})) \hookrightarrow \mathcal{S}(\mathbb{A}^{\perp})$, for $\beta \in \bigcup \mathcal{B}^{\perp}(b)$, one considers $y(b|\langle \beta \rangle) \in \mathcal{S}(\mathbb{B}^{\perp})$ and reasons analogously to show that $\alpha \in \bigcup \mathcal{A}^{\perp}(a)$. $\square$
**7.4. Stabilized presheaves on Boolean kits.** We now focus on categories of stabilized presheaves associated with Boolean kits and discuss the additional properties which hold there. A major difference with the kit case is the existence in $\mathcal{S}(\mathbb{A}, \mathcal{A})$ of all non-empty limits and filtered colimits. For the latter, we use that kits are closed under lubs of directed sets of subgroups.

**Lemma 7.10.** For a Boolean kit $(\mathbb{A}, \mathcal{A})$, $\mathcal{S}(\mathbb{A}, \mathcal{A})$ has filtered colimits.

The case of non-empty limits is immediate given the following:

**Lemma 7.11.** For a Boolean kit $(\mathbb{A}, \mathcal{A})$ and a morphism $X \xrightarrow{f} Y$ in $\mathcal{P}(\mathbb{A})$, if $Y \in \mathcal{S}(\mathbb{A}, \mathcal{A})$ then $X \in \mathcal{S}(\mathbb{A}, \mathcal{A})$.

*Proof idea.* For $a \in \mathbb{A}$ and $x \in X(a)$, $\mathrm{Stab}(x) \subseteq \mathrm{Stab}(f_a x) \in \mathcal{A}(a)$, and Boolean kits are closed under subgroups. $\square$

**Corollary 7.12.** For a Boolean kit $(\mathbb{A}, \mathcal{A})$, the embedding $\mathcal{S}(\mathbb{A}, \mathcal{A}) \hookrightarrow \mathcal{P}(\mathbb{A})$ creates isomorphisms, coproducts, filtered colimits, epimorphisms and non-empty limits.

*Proof.* Let $\{X_i\}_{i \in I}$ be a finite set of presheaves in $\mathcal{S}(\mathbb{A})$. We show that their coproduct in $\mathcal{P}\mathbb{A}$ is an element of $\mathcal{S}(\mathbb{A})$. For $(i, x) \in (\coprod_{i \in I} X_i)(a) = \coprod_{i \in I} X_i(a)$, $\mathrm{Stab}_{\coprod_{i \in I} X_i}(i, x) = \mathrm{Stab}_{X_i}(x)$ which is in $\mathcal{A}(a)$, so we are done.

Let $D : \mathbb{I} \to \mathcal{S}(\mathbb{A})$ be a filtered diagram. Denote by $X_i$ the presheaf $D(i)$ for $i \in \mathbb{I}$ and write $X$ for the colimit of $D$. Let $a$ be in $\mathbb{A}$, for every $x \in X(a)$, there exists $i \in \mathbb{I}$ and $y \in X_i(a)$ such that $(\mathrm{inj}_i)_a(y) = x$, where $\mathrm{inj}_i : X_i \to X$ denotes the cocone component. By naturality of $\mathrm{inj}_i$, if $\alpha : a \to a$ is in $\mathrm{Stab}_X(x)$ then $(\mathrm{inj}_i)_a(y\alpha) = (\mathrm{inj}_i)_a(y)$. Since $\mathbb{I}$ is filtered, there exists $j \in \mathbb{I}$ and $f : i \to j$ such that $D(f)_a(y \cdot \alpha) = D(f)_a(y)$. Hence, $\alpha \in \mathrm{Stab}_{X_j}(D(f)_a(y))$ so $\alpha$ is in $\bigcup \mathcal{A}(a)$ as desired.

We show that a morphism $e : X \Rightarrow Y$ is an epimorphism in $\mathcal{S}(\mathbb{A})$ if and only if its components $e_a : X(a) \to Y(a)$ are surjective for all $a \in \mathbb{A}$. Assume that there exists $a \in \mathbb{A}$ and $y \in Y(a)$ such that for all $x \in X(a)$, $e_a(x) \neq y$. By Lemma 7.5, $Y \cong \coprod_{i \in I} y(a_i|G_i)$ where each $G_i$ is a group in $\mathcal{A}(a_i)$. Let $j \in I$ be such that $y$ is in the component $y(a_j|G_j)(a)$. We show that for all $b \in \mathbb{A}$ and $z \in y(a_j|G_j)(b)$, $z$ is not in the image of $e_b$. Assume that there exists $x \in X(b)$ such that $e_b(x) = z$, then for any representative $\alpha \in \mathbb{A}(a, a_j)$ of the equivalence class $y$ and $\beta \in \mathbb{A}(b, a_j)$ of the equivalence class $z$, we obtain by naturality of $e$ that

$$e_a(x \cdot (\beta^{-1}\alpha)) = (e_b(x)) \cdot (\beta^{-1}\alpha) = [\beta] \cdot (\beta^{-1}\alpha) = [\beta\beta^{-1}\alpha] = [\alpha] = y.$$

Hence, we can factor $e$ as

$$X \longrightarrow \sum_{i \neq j} y(a_i|G_i) \longleftarrow \sum_{i \in I} y(a_i|G_i) \cong Y$$

Let $\mathrm{inj}_Y : Y \to Y + 1$ be the left hand coproduct inclusion and let $f : Y \to Y + 1$ be the natural transformation whose components $f_a$ are given by

$$\sum_{i \in I} y(a_i|G_i)(a) \ni (i, y) \mapsto \begin{cases} \mathrm{inj}_a(i, y) \in \{1\} \times Y(a) & \text{if } i \neq j \\ (2, \star) \in \{2\} \times 1(a) & \text{if } i = j \end{cases}$$

It is immediate that $\mathrm{inj}_Y e = fe$ but we do not have $\mathrm{inj}_Y = f$ contradicting the assumption of $e$ being an epimorphism. Hence, we must have that $e$ is pointwise surjective as desired. $\square$
On the other hand, the category $\mathcal{S}(\mathbb{A}, \mathcal{A})$ has a terminal object (an empty limit) only if $\mathcal{A}$ is maximal:

**Proposition 7.13.** For a Boolean kit $(\mathbb{A}, \mathcal{A})$, the following are equivalent.

(1) The terminal presheaf is in $\mathcal{S}(\mathbb{A}, \mathcal{A})$.

(2) For all $a \in \mathbb{A}$, $\mathcal{A}(a) = \{G \mid G \le \text{End}(a)\}$.

(3) $\mathcal{S}(\mathbb{A}, \mathcal{A}) = \mathcal{P}(\mathbb{A})$.

*Proof.*

• (1 $\Rightarrow$ 2) Let $a$ be in $\mathbb{A}$ and $G$ be a subgroup of $\mathbb{A}(a, a)$. Since $y(a|G)$ is in $\mathcal{S}(\mathbb{A})$ by assumption and $\text{Stab}(y(a|G)) = \{K \mid K \le G\}$, we obtain that $G \in \mathcal{A}(a)$ as desired.

• (2 $\Rightarrow$ 3) Let $1_{\mathbb{A}} : \mathbb{A}^{\text{op}} \to \text{Set}$ denote the terminal presheaf. For all $a \in \mathbb{A}$, $\text{Stab}(1_{\mathbb{A}})(a) = \{G \le \mathbb{A}(a, a) \mid a \in \mathbb{A}\}$ which implies that $1_{\mathbb{A}}$ is in $\mathcal{S}(\mathbb{A})$ by definition.

• (3 $\Rightarrow$ 1) Direct consequence of Lemma 7.11. $\square$

<figure><img src="image_5.png" /></figure>

We additionally note that for a Boolean kit $(\mathbb{A}, \mathcal{A})$, the Yoneda embedding $\mathbb{A} \to \mathcal{P}(\mathbb{A})$ factors through the inclusion $\iota_{\mathcal{A}} : \mathcal{S}(\mathbb{A}, \mathcal{A}) \hookrightarrow \mathcal{P}(\mathbb{A})$ via an embedding $\mathbb{A} \hookrightarrow \mathcal{S}(\mathbb{A}, \mathcal{A})$ which we denote $y_{\mathcal{A}}$. This holds because Boolean kits contain all trivial subgroups, and for an object $a$ of a groupoid $\mathbb{A}$ we have $y(a|\{\text{id}_a\}) \cong y(a)$.

We continue our development in the next section and introduce *stable functors*. We will show that for a stable species $P$, the mapping $P \mapsto \tilde{P}$ where $\tilde{P} = (\text{Lan}_s P)_{\iota_A}$ induces an equivalence between the hom-category of stable species and that of stable functors. Among the stable functors we will then identify the *linear* ones, and show they correspond to stabilized profunctors.

## 8. STABLE FUNCTORS

**8.1. Local right adjoints and generic factorizations.** The notion of stability in domain theory is often stated by means of a *minimal data property* first put forward by Berry [Ber78]:

**Definition 8.1 (Berry).** For cpos $(A, \le_A)$ and $(B, \le_B)$, a Scott-continuous function $f : A \to B$ is *stable* if for every $x \in A$ and $y \in B$ such that $y \le_B fx$, there exists a unique minimal $x_0 \in A$ such that $x_0 \le_A x$ and $y \le_B fx_0$.

For $x$ and $y$ as in the definition, $x_0$ has an operational meaning as the unique minimal amount of information used from $x$ to produce the output $y$. We denote this minimal element $x_0$ by $m(f, x, y)$. It is less well-known that the points $m(f, x, y)$ determine a family of *local* left adjoints to the restriction $f_x : A/x \to B/f(x)$ between the slices $A/x = \{x' \in A \mid x' \le_A x\}$ and $B/f(x) = \{y \in B \mid y \le_B f(x)\}$:

$$ \begin{tikzcd} A/x \arrow[r, "f_x"] \arrow[d, "\cong"] & B/f(x) \arrow[d, "\top"] \\ m(f, a, -) \arrow[r, "\cong"] & \phantom{B/f(x)} \end{tikzcd} $$

This condition is equivalent to stability.

**Lemma 8.2.** For cpos $(A, \le_A)$ and $(B, \le_B)$, a Scott-continuous function $f : A \to B$ is stable if and only if for every $x \in A$, the restriction $f_x : A/x \to B/fx$ has a left adjoint.
For our purposes, this characterization has the advantage that the existence of local adjoints may be considered in full generality:

**Definition 8.3.** For categories $\mathcal{A}$ and $\mathcal{B}$, a functor $T : \mathcal{A} \to \mathcal{B}$ is said to be a *local right* (resp. *left*) adjoint if for every object $a \in \mathcal{A}$, the induced functor $T_a : \mathcal{A}/a \to \mathcal{B}/T(a)$ is a right (resp. left) adjoint.

This notion is related to the *multiadjoint functors* initially developed by Diers [Die77] (see also [CJ95, Web04, Web07, Osm20, GK13]). Finitary local right adjoints are precisely the normal functors considered by Girard [Gir88] and Hasegawa [Has02], and the relevance of this notion to stable domain theory was further emphasized by Lamarche [Lam88] and Taylor [Tay89]. The extensional theory of stable species of structures fits into this line of research:

**Definition 8.4.** For kits $\mathcal{A}$ and $\mathcal{B}$, a functor $S(\mathcal{A}) \to S(\mathcal{B})$ is called *stable* when it is a finitary, local right adjoint functor that preserves epimorphisms.

The requirement of preserving epimorphisms will become clear as we construct a pseudo-inverse to the mapping $P \mapsto \tilde{P}$. Epi-preserving functors are of known significance in this area since, as shown by Fiore [Fio14], analytic functors between presheaf categories over groupoids may be characterized as finitary functors preserving *wide quasi-pullbacks*; this forces the preservation of epis.

We note, additionally, that the local right adjoint property ensures that stable functors preserve *wide pullbacks*, connecting with yet another presentation of stable functions in Berry's theory, as Scott continuous functions preserving bounded meets.

**Example 8.5.** In a cartesian closed and extensive category, such as a topos, the finite product and finite coproduct functors are stable. In connection to this, we discuss the prototypical non-stable, and hence non-sequential, function from Berry's stable domain theory [Ber78]. To this end, let $S$ be the Sierpinski space $(0 \subset 1)$ and, for $Bool = \{\mathbf{f}, \mathbf{t}\}$, consider the *parallel-or* function $por: S^{\mathbf{Bool}} \times S^{\mathbf{Bool}} \to S^{\mathbf{Bool}}$ defined as the least monotone function such that: $por(\{\mathbf{f}\}, \{\mathbf{f}\}) = \{\mathbf{f}\}$ and $por(\{\mathbf{t}\}, \{\mathbf{t}\}) = por(\{\}, \{\mathbf{t}\}) = \{\mathbf{t}\}$.

Parallel-or is not realizable as a stable functor at the categorical level in the strong sense that there is no stable functor $F: \mathbf{Set}^{\mathbf{Bool}} \times \mathbf{Set}^{\mathbf{Bool}} \to \mathbf{Set}^{\mathbf{Bool}}$ such that $F(0, 0) = 0$ and $F(y(\mathbf{t}), 0) = F(0, y(\mathbf{t})) = F(y(\mathbf{t}), y(\mathbf{t})) = y(\mathbf{t})$. Indeed, such functors do not preserve the pullback

<figure><img src="image_6.png" /></figure>

and thus induce local functors $F/(y(\mathbf{t}), y(\mathbf{t})) : \mathbf{Set}^{\mathbf{Bool}} \times \mathbf{Set}^{\mathbf{Bool}}/(y(\mathbf{t}), y(\mathbf{t})) \to \mathbf{Set}^{\mathbf{Bool}}/y(\mathbf{t})$ that fail to be right adjoints.

However, the generalization from domains to categories allows for an intensional quantitative interpretation of parallel or. Indeed, for $K: \mathbf{Set} \to S$ the *collapse* functor mapping a set to 0 if it is empty and to 1 otherwise, we have a stable functor

$$P(X, Y) = (X_{\mathbf{f}} \times Y_{\mathbf{f}}, X_{\mathbf{t}} + Y_{\mathbf{t}})$$
lifting *por* as follows:

$$ \begin{array}{ccc} \mathbf{Set}^{\mathbf{Bool}} \times \mathbf{Set}^{\mathbf{Bool}} & \xrightarrow{P} & \mathbf{Set}^{\mathbf{Bool}} \\ K^{\mathbf{Bool}} \times K^{\mathbf{Bool}} \searrow & & K^{\mathbf{Bool}} \\ \mathcal{S}^{\mathbf{Bool}} \times \mathcal{S}^{\mathbf{Bool}} \underset{por}{\longrightarrow} & & \mathcal{S}^{\mathbf{Bool}} \end{array} $$

For kits $\mathcal{A}$ and $\mathcal{B}$ and a local right adjoint functor $T : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$, one may unfold for each $X \in \mathcal{S}(\mathcal{A})$ the right adjoint property for $T_X$: for every $h : Y \to TX$, there exist $f : X_0 \to X$ and $g : Y \to TX_0$ such that $h$ factorizes as follows:

$$ Y \underset{g}{\overset{h}{\rightleftharpoons}} T(X_0) \underset{T(f)}{\overset{T(X)}{\rightleftharpoons}} $$

Note the analogy with Definition 8.1. The minimality requirement for $X_0$ is represented here by a universal property known as *genericity*, which $g$ must additionally satisfy. The idea is to exhibit $T(f) \circ g$ as initial in the category of factorizations of $h$ of the form $T(-) \circ -$. These correspond to the normal forms studied by Girard and Hasegawa [Gir88, Has02].

**Definition 8.6.** Suppose that $T : \mathcal{A} \to \mathcal{B}$ is a functor between categories $\mathcal{A}$ and $\mathcal{B}$. A morphism $g : b \to T(a)$ in $\mathcal{B}$ is said to be *generic* if for every commuting square as on the left below, there exists a unique morphism $k : a \to a'$ in $\mathcal{A}$ making the two triangles on the right commute.

<figure><img src="image_7.png" /></figure>

We can then derive a standard result:

**Theorem 8.7.** A functor $T : \mathcal{A} \to \mathcal{B}$ is a local right adjoint if and only if it admits generic factorizations, in the sense that every morphism $h : b \to T(a)$ has a factorisation $h = T(f) \circ g$ with $g$ generic.

Generic morphisms (elsewhere known as *strict generic* [Web04] or *candidates* [Tay89]) provide the elements in the construction of a stable species from a stable functor. What we obtain is analogous to the *trace* of a stable function in Berry's work [Ber78] and closely related to Taylor's trace [Tay98]. It is appropriate here to use the same terminology. In the case of combinatorial or generalized species, the map $k$ in Definition 8.6 is not required to be unique and one works with the corresponding notion of *generic elements* introduced by Joyal [Joy86] and generalized by Fiore [Fio14] in order to construct a species from an analytic functor.

To show that stable species induce stable functors via the mapping $P \mapsto \tilde{P}$, we reduce the proof of admitting generic factorizations to only considering generic factorizations relative to representables:

**Lemma 8.8.** Let $T : \mathcal{A} \to \mathcal{B}$ be a functor.
(1) For diagrams $A: \mathbb{I} \to \mathbb{A}$ and $B: \mathbb{I} \to \mathbb{B}$, and a natural transformation $g: B \Rightarrow TA: \mathbb{I} \to \mathbb{B}$, if $g_i: B_i \to T(A_i)$ is generic for all $i \in \mathbb{I}$ then so is the induced composite

$$k = \operatorname{colim}(B) \xrightarrow{\operatorname{colim}(g)} \operatorname{colim}(TA) \xrightarrow{[\operatorname{inj}_i]_{i \in \mathbb{I}}} T(\operatorname{colim}A).$$

(2) For $b \in \mathbb{B}$, a diagram $A: \mathbb{I} \to \mathbb{A}$, and a cone $g: b \Rightarrow TA: \mathbb{I} \to \mathbb{B}$, if $g_i: b \to T(A_i)$ is generic for all $i \in \mathbb{I}$ then so are the composites

$$b \xrightarrow{g_i} T(A_i) \xrightarrow{T(\operatorname{inj}_i)} T(\operatorname{colim}(A))$$

for every $i \in \mathbb{I}$.

*Proof.*

(1) Let $(\operatorname{inj}_i: B_i \to \operatorname{colim}(B))_{i \in \mathbb{I}}$ be a colimiting cocone. Consider $l: \operatorname{colim}(B) \to T(d)$ in $\mathbb{B}$ and $h: \operatorname{colim}(A) \to c$, $f: d \to c$ in $\mathbb{A}$ such that $T(h) \circ k = T(f) \circ l$; equivalently, $T(h) \circ T(\operatorname{inj}_i) \circ g_i = T(f) \circ l \circ \operatorname{inj}_i$ for all $i \in \mathbb{I}$. Since each $g_i$ is generic, there exists, for every $i \in \mathbb{I}$, a unique morphism $e_i: A_i \to d$ such that $h \circ \operatorname{inj}_i = f \circ e_i$ and $T(e_i) \circ g_i = l \circ \operatorname{inj}_i$.

<figure><img src="image_8.png" /></figure>

One can show that $(e_i: A_i \to d)_{i \in \mathbb{I}}$ is a cocone of $A$. So there exists a unique morphism $e: \operatorname{colim}(A) \to d$ such that $e \circ \operatorname{inj}_i = e_i$; from which it follows that $f \circ e = h$. Moreover, $T(e) \circ k = l$ because $T(e) \circ k \circ \operatorname{inj}_i = l \circ \operatorname{inj}_i$ for all $i \in \mathbb{I}$. This establishes existence. As for uniqueness, if $e': \operatorname{colim}(A) \to d$ has the required property of $k$ with respect to $h$, $f$, $l$ then each $e' \circ \operatorname{inj}_i$ has the generic property of $g_i$ with respect to $h \circ \operatorname{inj}_i$, $f$, $l \circ \operatorname{inj}_i$ making $e' \circ \operatorname{inj}_i = e_i$ and therefore $e' = e$.

(2) Let $i \in \mathbb{I}$ and assume that there exists $l: b \to T(d)$, $k: \operatorname{colim}(A) \to c$ and $f: d \to c$ such that $T(k) \circ T(\operatorname{inj}_i) \circ g_i = T(f) \circ l$. Since $g_i$ is generic, there exists a unique $e_i: A_i \to d$ such that $k \circ \operatorname{inj}_i = f \circ e_i$ and $T(e_i) \circ g_i = l$.

<figure><img src="image_9.png" /></figure>

One can check that $(e_i: A_i \to d)_{i \in \mathbb{I}}$ is a cocone of $A$. Hence, there exists a unique morphism $e: \operatorname{colim}(A) \to d$ such that $e \circ \operatorname{inj}_i = e_i$ for all $i \in \mathbb{I}$. Since $(f \circ e_i: a_i \to c)_{i \in \mathbb{I}}$ is a cocone of $A$, there exists a unique $q: \operatorname{colim}(A) \to c$ such that $q \circ \operatorname{inj}_i = f \circ e_i$ for all $i \in \mathbb{I}$. Both $k$ and $f \circ e$ verify this condition which implies that $k = f \circ e$. We also have
that $T(e) \circ T(\mathrm{inj}_i) \circ g_i = T(e_i) \circ g_i = l$. To show that $T(\mathrm{inj}_i) \circ g_i$ is generic, it remains
to show that $e : \mathrm{colim}(A) \to d$ is the unique morphism that makes the two diagrams
below commute.

<figure><img src="image_10.png" /></figure>

Assume that there exists $e' : \mathrm{colim}(A) \to d$ such that $k = f \circ e'$ and $T(e') \circ T(\mathrm{inj}_i) \circ g_i = l$.
We then have that $e' \circ \mathrm{inj}_i = e_i$ for all $i \in \mathbb{I}$ by genericity of the $g_i$'s which implies that
$e' = e$ by the universal property of the colimit. $\square$

**Proposition 8.9.** Let $T : \mathbb{A} \to \mathbb{B}$ be a functor. For a diagram $B : \mathbb{I} \to \mathbb{B}$, if $T$ admits generic factorizations relative to $b_i$ for all $i \in \mathbb{I}$ then it admits generic factorizations relative to $\mathrm{colim}(B)$ whenever this exists.

*Proof.* Assume that $\mathrm{colim}(B)$ exists in $\mathbb{B}$ and let $f : \mathrm{colim}(B) \to T(a)$ be a morphism in $\mathbb{B}$.
By hypothesis, each $f_i := f \circ \mathrm{inj}_i : b_i \to T(a)$ can be factored as:

$$b_i \xrightarrow{g_i} T(c_i) \xrightarrow{T(h_i)} T(a)$$

where $g_i$ is generic. Define the diagram $C : \mathbb{I} \to \mathbb{A}$ as follows: $C(i) := c_i$ for $i \in \mathbb{I}$ and for a morphism $e : i \to j \in \mathbb{I}$, $C(e)$ is the unique morphism $c_i \to c_j$ obtained from the genericity of $g_i$ in the square below:

<figure><img src="image_11.png" /></figure>

By Lemma 8.8.1, $[T(\mathrm{inj}_i)]_{i \in \mathbb{I}} \circ \mathrm{colim}(g) : \mathrm{colim}(B) \to \mathrm{colim}(C)$ is generic. Let $[h] : \mathrm{colim}(C) \to a$ be the mediating morphism induced by the cocone $(h_i : c_i \to a)_{i \in \mathbb{I}}$. Both $f$ and $T([h]) \circ [T(\mathrm{inj}_i)]_{i \in \mathbb{I}} \circ \mathrm{colim}(g)$ verify the conditions of the mediating morphism $\mathrm{colim}(B) \to T(a)$ induced by the cocone $(T(h_i) \circ T(\mathrm{inj}_i) \circ g_i : b_i \to T(a))_{i \in \mathbb{I}}$ which implies that $f = T([h]) \circ [T(\mathrm{inj}_i)]_{i \in \mathbb{I}} \circ \mathrm{colim}(g)$ as desired. $\square$

Recall that a generalized species $P : \Sigma\mathbb{A} \dashrightarrow \mathbb{B}$ induces an analytic functor $\mathrm{Lan}_s P : \mathcal{P}\mathbb{A} \to \mathcal{P}\mathbb{B}$ mapping a presheaf $X \in \mathcal{P}\mathbb{A}$ and an object $b \in \mathbb{B}$ to $(\mathrm{Lan}_s P)(X)(b)$ given by the following coend formula:

$$\int^{u=\langle a_1, \dots, a_n \rangle \in \Sigma \mathbb{A}} P(b, u) \times \mathcal{P}\mathbb{A}(s(u), X) \cong \int^{u=\langle a_1, \dots, a_n \rangle \in \Sigma \mathbb{A}} P(b, u) \times \prod_{i=1}^{n} X(a_i)$$

which explicitly consists of equivalences classes of triples $u \in \Sigma\mathbb{A}$, $p \in P(b, u)$, $\bar{x} \in \mathcal{P}\mathbb{A}(s(u), X) \cong X^{\Sigma}(u)$ that we denote by $p \underset{\bar{x}}{\dashv} \bar{x}$. Thus, $p \underset{\bar{x}}{\dashv} \bar{x} = q \underset{\bar{y}}{\dashv} \bar{y}$ if and only if there exists $\alpha : u \to v$ in $\Sigma\mathbb{A}$ such that $\bar{y} \cdot \alpha = \bar{x}$ and $\alpha \cdot p = q$.
The Boolean kit ($\Sigma\mathfrak{A}$, !$\mathfrak{A}$) in Definition 6.4 has an extensional characterization in terms of stabilized presheaf which we will use in the proofs:

**Lemma 8.10.** For a kit $\mathfrak{A} = (\mathfrak{A}, \mathcal{A})$, the following equality holds for all $u \in \Sigma\mathfrak{A}$:

$$ !\mathfrak{A}(u) = \{G \leq \text{Endo}(u) \mid \exists X \in \mathcal{S}(\mathfrak{A}), G \in \text{Stab}(X^{\Sigma}(u))\}^{\perp\perp}. $$

**Lemma 8.11.** For Boolean kits $\mathfrak{A}, \mathfrak{B}$, a presheaf $X \in \mathcal{S}(\mathfrak{A})$ and a stable species $P : !\mathfrak{A} \to \mathfrak{B}$, if two elements $p \bowtie \bar{x}$ and $q \bowtie \bar{y}$ in $(\text{Lan}_s P)(X)(b)$ are equal for some $b \in \mathfrak{B}$, then there exists a unique $\alpha : u \to v$ in $\Sigma\mathfrak{A}$ such that $\bar{y} \cdot \alpha = \bar{x}$ and $\alpha \cdot p = q$.

*Proof.* Assume that for $p \in P(b, u)$, $q \in P(b, v)$, $\bar{x} \in X^{\Sigma}(u)$ and $\bar{y} \in X^{\Sigma}(v)$, we have the equality $p \bowtie \bar{x} = q \bowtie \bar{y}$. The existence of $\alpha : u \to v$ in $\Sigma\mathfrak{A}$ such that $\bar{y} \cdot \alpha = \bar{x}$ and $\alpha \cdot p = q$ follows from the pointwise definition of the coend. For uniqueness, assume that there exists $\beta : u \to v$ such that $\bar{y} \cdot \beta = \bar{x}$ and $\beta \cdot p = q$ as well. The equality $\alpha \cdot p = \beta \cdot p$ implies that $\beta^{-1}\alpha \cdot p = p$ and since $\text{id}_b$ is in $\mathfrak{B}^{\perp}(b)$, we have $\beta^{-1}\alpha \in \bigcup (!\mathfrak{A})^{\perp}(u)$ as $P$ is a stable species. On the other hand, $\bar{y} \cdot \alpha = \bar{y} \cdot \beta$ implies that $\beta^{-1}\alpha$ is in $\text{Stab}(X^{\Sigma}(u))$ which entails that $\beta^{-1}\alpha \in \bigcup (!\mathfrak{A})(u)$ by Lemma 8.10. Hence, $\beta^{-1}\alpha = \text{id}$ as desired. $\square$

**Proposition 8.12.** For a stable species $P : !\mathfrak{A} \to \mathfrak{B}$, the restricted left Kan extension $\tilde{P} = (\text{Lan}_s P)_{\iota_{\mathfrak{A}}} : \mathcal{S}(\mathfrak{A}) \to \mathcal{P}\mathfrak{B}$ factors through the inclusion $\mathcal{S}(\mathfrak{B}) \hookrightarrow \mathcal{P}(\mathfrak{B})$. Furthermore, the resulting functor $\tilde{P} : \mathcal{S}(\mathfrak{A}) \to \mathcal{S}(\mathfrak{B})$ is stable.

*Proof.* To prove that $(\text{Lan}_s P)_{\iota_{\mathfrak{A}}}$ restricts to a functor $\mathcal{S}(\mathfrak{A}) \to \mathcal{S}(\mathfrak{B})$, we show that for all $X \in \mathcal{S}(\mathfrak{A})$ and $b \in \mathfrak{B}$, the stabilizer of every element in $\text{Lan}_s P X(b) = \int_{u \in \Sigma\mathfrak{A}} P(b, u) \times X^{\Sigma}(u)$ is in $\mathfrak{B}(b)$. Let $t = p \bowtie \bar{x}$ in $\text{Lan}_s P X(b)$. For every $\beta : b \to b$ in $\text{Stab}(t)$, we have $(p \cdot \beta) \bowtie \bar{x} = p \bowtie \bar{x}$, i.e. there exists $\alpha : u \to u$ in $\Sigma\mathfrak{A}$ such that $\alpha \cdot p \cdot \beta = p$ and $\bar{x} \cdot \alpha = \bar{x}$. Since $X$ is in $\mathcal{S}(\mathfrak{A})$ and $\alpha$ is in $\text{Stab}(X^{\Sigma}(u))$, we must have $\alpha \in \bigcup !\mathfrak{A}(u)$ and since $P$ is a stable species, it implies that $\beta \in \bigcup \mathfrak{B}(b)$ as desired. It remains to show that the functor $\tilde{P} : \mathcal{S}(\mathfrak{A}) \to \mathcal{S}(\mathfrak{B})$ is stable.

The functor $\text{Lan}_s P : \mathcal{P}\mathfrak{A} \to \mathcal{P}\mathfrak{B}$ is analytic and therefore is finitary and preserves quasi-pullbacks (and hence epimorphisms) [Fio14]. Since the embeddings $\iota_{\mathfrak{A}} : \mathcal{S}\mathfrak{A} \to \mathcal{P}\mathfrak{A}$ and $\iota_{\mathfrak{B}} : \mathcal{S}\mathfrak{B} \to \mathcal{P}\mathfrak{B}$ create epimorphisms and filtered colimits, $\tilde{P}$ is epi-preserving and finitary.

It remains to show that $\tilde{P}$ admits generic factorizations. By Proposition 8.9, it suffices to show that $\tilde{P}$ admits generic factorizations relative to representables. Consider a morphism $yb \to \tilde{P}(X)$ in $\mathcal{S}(\mathfrak{B})$, it is of the form $p \bowtie \bar{x}$ with $p \in P(b, u)$ and $\bar{x} : su \to X$ for some $u \in \Sigma\mathfrak{A}$. We show that

$$ yb \xrightarrow{p \bowtie \text{id}} \tilde{P}(su) \xrightarrow{\tilde{P}(\bar{x})} \tilde{P}(X) $$

is a generic factorization for $p \bowtie \bar{x}$. The equality $p \bowtie \bar{x} = \tilde{P}(\bar{x})(p \bowtie \text{id})$ is immediate, it remains to prove that $p \bowtie \text{id}$ is generic.

Assume that there exist $Y, Z \in \mathcal{S}(\mathfrak{A})$ and morphisms $p' \bowtie \bar{y} : yb \to \tilde{P}(Y)$ and $f : Y \to Z$ and $\bar{z} : su \to Z$ such that the following diagram commutes in $\mathcal{S}(\mathfrak{B})$:
<figure><img src="image_12.png" /></figure>

The equality $\tilde{P}(f)(p' \bowtie \bar{y}) = p \bowtie \bar{z}$ is equivalent to $p' \bowtie f\bar{y} = p \bowtie \bar{z}$ which implies by Lemma 8.11 that there exists a unique $\alpha : u \to v$ in $\Sigma A$ such that $(f\bar{y}) \cdot \alpha = \bar{z}$ and $\alpha \cdot p = p'$. We then have $\tilde{P}(\bar{y} \cdot \alpha)(p \bowtie \bar{y} \cdot \alpha) = \alpha \cdot p \bowtie \bar{y} = p' \bowtie \bar{y}$. It remains to show uniqueness, assume that there exists $\bar{t} : su \to Y$ such that $f\bar{t} = \bar{z}$ and $\tilde{P}(\bar{t})(p \bowtie \bar{y} \cdot \alpha) = p' \bowtie \bar{y}$ i.e. $p \bowtie \bar{t} = p' \bowtie \bar{y}$.

<figure><img src="image_13.png" /></figure>

It implies that there exists $\beta : u \to v$ such that $\bar{y} \cdot \beta = \bar{t}$ and $\beta \cdot p = p'$. Hence, $(f\bar{y}) \cdot \alpha = f\bar{t} = \bar{z}$ which implies that $\alpha = \beta$ so that $\bar{t} = \bar{y} \cdot \alpha$ as desired. $\square$

Analogously to the trace operator for stable functions, we now define a trace functor providing an inverse to the operation $P \mapsto \tilde{P}$ by using the generic factorization property.

**Definition 8.13.** Consider Boolean kits $\mathcal{A}$ and $\mathcal{B}$ and a stable functor $T : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$. The trace of $T$ is the profunctor $\mathbf{Tr}(T) : \mathcal{B}^{\circ} \times \Sigma \mathcal{A} \to \mathbf{Set}$ with object mapping

$$ \mathbf{Tr}(T)(b, \langle a_i \rangle_{i \in [n]}) = \{ g : yb \to T(\coprod_i ya_i) \mid g \text{ is generic} \} $$

and functorial action given by composition.

The trace of a stable functor is a stable species of structures:

**Proposition 8.14.** For Boolean kits $\mathcal{A}$ and $\mathcal{B}$ and a stable functor $T : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$, $\mathbf{Tr}(T) \in \mathbf{SEsp}(\mathcal{A}, \mathcal{B})$.

*Proof.* We first need to show that $\mathbf{Tr}(T)$ is indeed a species, i.e. for $t : b \to T(s(u))$ generic and morphisms $\alpha \in \Sigma A(u, u)$, $\beta \in \mathcal{B}(b, b)$, $\alpha \cdot t \cdot \beta = T(s(\alpha)) \circ t \circ \beta$ is also generic which holds since generic elements are stable under precomposition or postcomposition by isomorphisms. We now prove that $\mathbf{Tr}(T)$ is a stable species: assume that $\alpha \cdot t \cdot \beta = t$ i.e. the following square commutes in $\mathcal{S}(\mathcal{B})$:

<figure><img src="image_14.png" /></figure>
* Assume that $\alpha \in \bigcup!\mathcal{A}(u)$, using Lemmas 4.9 and 8.10, it implies that for all $n \in \mathbb{N}$, $\alpha^n = \text{id}$ or there exists $m \in \mathbb{N}$ and $\text{id} \neq \alpha^{nm} \in \text{Stab}(X^{\Sigma}(u))$ for some $X \in \mathcal{S}(\mathcal{A})$. We want to show that $\beta$ is in $\bigcup\mathcal{B}(b) = \bigcup\mathcal{B}^{\perp}(b)$ i.e. for all $n \in \mathbb{N}$, $\beta^n = \text{id}$ or there exists $m \in \mathbb{N}$ such that $\text{id} \neq \beta^{nm} \in \bigcup\mathcal{B}(b)$. Equivalently, we show that for all $n \in \mathbb{N}$, $\beta^n = \text{id}$ or there exist $m \in \mathbb{N}$ and $Y \in \mathcal{S}(\mathbb{B})$ with $\text{id} \neq \beta^{nm} \in \text{Stab}(Y(b))$.

Let $n \in \mathbb{N}$ and assume that $\beta^n \neq \text{id}$, if $\alpha^n = \text{id}$, then $t \cdot \beta^n = t$ which implies that $\beta^n$ is in $\text{Stab}(T(s(u)))$. Since $T(s(u))$ is in $\mathcal{S}(\mathbb{B})$, we can take $m := 1$ and obtain the desired result. If there exist $m \in \mathbb{N}$ and $X \in \mathcal{S}(\mathcal{A})$ such that $\text{id} \neq \alpha^{nm} \in \text{Stab}(X^{\Sigma}(u))$, then there exists $\bar{x} : s(u) \to X$ in $\mathcal{S}(\mathcal{A})$ (or equivalently $\bar{x} \in X^{\Sigma}(u)$) such that $\bar{x} \cdot \alpha^{nm} = \bar{x}$ which implies that the following diagram commutes in $\mathcal{S}(\mathbb{B})$:

<figure><img src="image_15.png" /></figure>

Hence, $\beta^{nm}$ is in $\text{Stab}(T(X)(b))$ and since $T(X)$ is in $\mathcal{S}(\mathbb{B})$, it only remains to show that $\beta^{nm} \neq \text{id}$. Assume that $\beta^{nm} = \text{id}$, then $\alpha^{nm} \cdot t = t$, so the following diagram commutes in $\mathcal{S}(\mathbb{B})$:

<figure><img src="image_16.png" /></figure>

since $t$ is generic, it implies that $\alpha^{nm} = \text{id}$ so $\beta^{nm} \neq \text{id}$ as desired.

* Assume now that $\beta \in \bigcup\mathcal{B}^{\perp}(b)$, we want to show that $\alpha \in \bigcup(!\mathcal{A})^{\perp}(u)$ i.e. for all $n$, if there exists $X' \in \mathcal{S}(\mathcal{A})$ such that $\alpha^n$ is in $\text{Stab}(X'^{\Sigma}(u))$, then $\alpha^n = \text{id}$. Assume that there exists $X' \in \mathcal{S}(\mathcal{A})$ such that $\alpha^n$ is in $\text{Stab}(X'^{\Sigma}(u))$, i.e. there exists $\bar{x}': s(u) \to X'$ in $\mathcal{S}(\mathcal{A})$ such that $\bar{x}' \cdot \alpha^n = \bar{x}'$ which implies that the following diagram commutes in $\mathcal{S}(\mathbb{B})$:

<figure><img src="image_17.png" /></figure>

Hence, $\beta^n \in \text{Stab}(T(X')(b))$ which implies that $\beta^n = \text{id}$ so that the following diagram commutes:
<figure><img src="image_18.png" /></figure>

Since $t$ is generic, we obtain that $\alpha^n = \text{id}$ as desired.

<figure><img src="image_19.png" /></figure>

We proceed to show that for a stable species $P \in \mathbf{SEsp}(\mathcal{A}, \mathcal{B})$, $\mathbf{Tr}(\tilde{P}) \cong P$, and for a stable functor $T : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$, $\bar{\mathbf{Tr}}(T) \cong T$.

**Lemma 8.15.** For a stable species $P : !\mathcal{A} \dashrightarrow \mathcal{B}$, the transformation $\eta : P \to \tilde{\mathbf{Tr}}(\tilde{P})$ whose components $\eta_{b,u} : P(b, u) \to \tilde{\mathbf{Tr}}(\tilde{P})(b, u)$ are given by

$$p \mapsto (p \underset{\bar{u}}{\boxtimes} \text{id}) : b \to \tilde{P}(s(u))$$

is a natural isomorphism.

*Proof.* We first need to show that $(p \underset{\bar{u}}{\boxtimes} \text{id}) : b \to \tilde{P}(s(u))$ is generic for the map $\eta_{b,u}$ to be well-defined. Assume that the diagram below commutes in $\mathcal{S}(\mathcal{B})$ for some morphisms $\bar{x} : s(u) \to X$, $f : Y \to X$ and $h : b \to \tilde{P}(Y)$:

<figure><img src="image_20.png" /></figure>

The morphism $h : b \to \tilde{P}(Y)$ corresponds to an element $(p' \underset{\bar{u}}{\boxtimes} \bar{y})$ where $p' \in P(b, u')$ and $\bar{y} : s(u') \to Y$. Since the diagram commutes, we have $p' \underset{\bar{u}}{\boxtimes} \bar{x} = p' \underset{\bar{u}}{\boxtimes} f\bar{y}$ i.e. there exists $\alpha : u \to u'$ in $\Sigma\mathcal{A}$ such that $\alpha \cdot p = p'$ and $f\bar{y}s(\alpha) = \bar{x}$. Define $k : s(u) \to Y$ to be $\bar{y}s(\alpha)$. We then have $fk = \bar{x}$ and $\tilde{P}(k)(p' \underset{\bar{u}}{\boxtimes} \text{id}) = p' \underset{\bar{u}}{\boxtimes} \bar{y}s(\alpha) = \alpha \cdot p' \underset{\bar{u}}{\boxtimes} \bar{y} = p' \underset{\bar{u}}{\boxtimes} \bar{y}$ as desired.

For uniqueness, assume that there exists $k' : s(u) \to Y$ such that $fk' = \bar{x}$ and $\tilde{P}(k')(p' \underset{\bar{u}}{\boxtimes} \text{id}) = p' \underset{\bar{u}}{\boxtimes} k' = p' \underset{\bar{u}}{\boxtimes} \bar{y}$. It implies that there exists $\beta : u \to u'$ in $\Sigma\mathcal{A}$ such that $\beta \cdot p = p'$ and $\bar{y}s(\beta) = k'$. Since $\text{id}_b \in \bigcup \mathcal{B}(b)^\perp$ and $\beta\alpha^{-1} \cdot p' = p'$, we have $\beta\alpha^{-1} \in \bigcup !\mathcal{A}(u')^\perp$. Now, $f\bar{y}s(\beta) = f\bar{y}s(\alpha)$ implies that $\beta\alpha^{-1}$ is in $\text{Stab}(X^\Sigma(u'))$. Since $X \in \mathcal{S}(\mathcal{A})$, we obtain that $\alpha = \beta$ as desired. Hence, $\eta_{u,b}$ is well-defined, it remains to show that it is injective and surjective.

For injectivity, if there are $p$ and $p'$ in $P(b, u)$ such that $p' \underset{\bar{u}}{\boxtimes} \text{id} = p' \underset{\bar{u}}{\boxtimes} \text{id}$ then there exists $\alpha : u \to u'$ such that $\alpha \cdot p = p'$ and $\alpha \circ \text{id} = \text{id}$ which implies that $p = p'$. For surjectivity, let $p' \underset{\bar{u}}{\boxtimes} \bar{z} : b \to \tilde{P}(s(u))$ be a generic map. Since the diagram below commutes, there exists a unique $k : s(u) \to s(v)$ in $\mathcal{S}(\mathcal{A})$ such that $\bar{z}k = \text{id}$ and $p' \underset{\bar{u}}{\boxtimes} k\bar{z} = p' \underset{\bar{u}}{\boxtimes} \text{id}$.
$$
\begin{tikzcd}
& & b \arrow[r, "(p \bowtie \mathrm{id})"'] \arrow[d, "(p \bowtie \bar{z})"'] & \tilde{P}(s(v)) \arrow[d, "\tilde{P}(\bar{z})"'] \\
(p \bowtie \bar{z}) \arrow[r, "\sim"] & \tilde{P}(s(u)) \arrow[r, "\sim"] & \tilde{P}(\mathrm{id}) & \\
& & & \\
& & & \tilde{P}(s(u))
\end{tikzcd}
$$

Since $p \bowtie \mathrm{id}$ is generic, we can apply the same reasoning and obtain that $\bar{z}$ has a left inverse as well and is therefore an isomorphism. By Lemma 8.17, there exists $\alpha : u \to u'$ in $\mathbb{A}$ such that $\bar{z} = s(\alpha)$. Hence, $p \bowtie \bar{z} = \alpha^{-1} \cdot p \bowtie \mathrm{id}$ which implies that $\eta_{b,u}$ is surjective as desired. $\square$

**Lemma 8.16.** For a Boolean kit $\mathbb{A}$ and presheaves $X$ and $Y$ in $\mathcal{S}(\mathbb{A})$, if $Y$ is a coproduct of representables $\coprod_{i \in I} Y(a_i)$ and there is a monomorphism $m : X \hookrightarrow Y$, then $X \cong \coprod_{j \in J} Y(a_j)$ where $J \subseteq I$.

*Proof.* By Lemma 7.5, $X$ is isomorphic to $\coprod_{j \in J} Y(b_j|G_j)$ where each $b_j \in \mathbb{A}$ and $G_j \in \mathcal{A}(b_j)$. Since $m$ is monic, $X$ is a free action, i.e. for all $a \in \mathbb{A}$, $x \in X(a)$ and $\alpha : a \to a$ such that $x \cdot \alpha = x$, we must have $\alpha = \mathrm{id}_a$. Indeed, $x \cdot \alpha = x$ implies $(m_a(x)) \cdot \alpha = m_a(x)$ which entails that $\alpha = \mathrm{id}_a$ since $Y$ is a free action. Hence, all the groups $G_j$ are trivial and $X \cong \coprod_{j \in J} Y(a_j)$. Now, since $\mathcal{P}\mathbb{A}(X, Y)$ is isomorphic to $\coprod_{\sigma:J \to I} \coprod_{j \in J} \mathbb{A}(b_j, a_{\sigma(j)})$, $m : X \to Y$ corresponds to a pair $(\sigma, (\alpha_j)_j)$ of a function $\sigma : I \to J$ and a family of isomorphisms $\alpha_j : b_j \to a_{\sigma(j)}$. Since $m$ is monic, $\sigma$ is injective and we obtain the desired result. $\square$

**Lemma 8.17.** For sequences $\langle a_1, \dots, a_n \rangle$, $\langle b_1, \dots, b_n \rangle$ in $\Sigma\mathbb{A}$, if there is an isomorphism $f : \coprod_{1 \le i \le n} Y(a_i) \cong \coprod_{1 \le i \le n} Y(b_i)$ in $\mathcal{P}\mathbb{A}$, then there exists a morphism $\alpha \in \Sigma\mathbb{A}$ such that $f = s(\alpha)$.

*Proof.* Immediate corollary of the isomorphism $\mathcal{P}\mathbb{A}(\langle a_i \rangle, \langle b_j \rangle) \cong \coprod_{\sigma:J \to I} \coprod_{j \in J} \mathbb{A}(b_j, a_{\sigma(j)})$. $\square$

**Lemma 8.18.** Let $\mathbb{A}$ and $\mathbb{B}$ be Boolean kits and $T : \mathcal{S}(\mathbb{A}) \to \mathcal{S}(\mathbb{B})$ be a stable functor. For every $X$ in $\mathcal{S}(\mathbb{A})$ and $t : b \to T(X)$ in $\mathcal{S}(\mathbb{B})$, there exists $u \in \Sigma\mathbb{A}$, $g : b \to T(s(u))$ generic and $\bar{x} : s(u) \to X$ such that $t = T(\bar{x})g$.

*Proof.* Since $T$ is stable, $t$ can be factored as $b \xrightarrow{g} T(Y) \xrightarrow{T(f)} T(X)$ where $g$ is generic. By Corollary 7.6, $Y$ is isomorphic to $\mathrm{colim}_{i \in I} \coprod_{j \in J_i} Y(a_{ij}|G_{ij})$ where each $G_{ij}$ is a finitely generated group in $\mathcal{A}(a_{ij})$ and $I$ is filtered. Since $T$ is finitary, we have

$$ T(Y) \cong \mathrm{colim}_{i \in I} T\left(\coprod_{j \in J_i} Y(a_{ij} | G_{ij})\right). $$

Since filtered colimits are computed pointwise in $\mathcal{S}(\mathbb{B})$, it implies that $g$ can be factored as

$$ b \xrightarrow{g'} T\left(\coprod_{j \in J} Y(a_j | G_j)\right) \xrightarrow{T(\mathrm{inj})} \mathrm{colim}_{i \in I} T\left(\coprod_{j \in J_i} Y(a_{ij} | G_{ij})\right). $$

For each group $G_j$, the projection morphism $q_j : ya_j \to y(a_j|G_j)$ is an epimorphism which implies that $q := \coprod_{j \in J} q_j : \coprod_{j \in J} ya_j \to \coprod_{j \in J} y(a_j|G_j)$ is also an epimorphism. Since $T$ is epi-preserving, we can factor $g'$ as

$$ b \xrightarrow{g''} T\left(\coprod_{j \in J} ya_j\right) \xrightarrow{q} T\left(\coprod_{j \in J} y(a_j|G_j)\right). $$
Since $g$ is generic, there exists a unique $h : Y \to \coprod_{j \in J} ya_j$ such that $injqh = \text{id}$ and $T(h)g = g''$.

<figure><img src="image_21.png" /></figure>

Since $h$ is split monic, by Lemma 8.16, we have $Y \cong \coprod_{k \in K} ya_k$ where $K \subseteq J$. $\square$

**Lemma 8.19.** For a stable functor $T : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$, the transformation $\varepsilon : \widetilde{\mathrm{Tr}}T \Rightarrow T$ whose components $\varepsilon_{X,b}$ are given by

$$ (t \underset{\bar{u}}{\otimes} \bar{x} : s(u) \to X) \mapsto T(\bar{x})t : b \to T(X) $$

is a natural isomorphism.

*Proof.* We first show that the map $\varepsilon_{X,b}$ is well-defined. For elements $t \underset{\bar{u}}{\otimes} \bar{x}$ and $t' \underset{\bar{u}}{\otimes} \bar{x}'$ in $\widetilde{\mathrm{Tr}}T(X, b)$, if $t \underset{\bar{u}}{\otimes} \bar{x} = t' \underset{\bar{u}}{\otimes} \bar{x}'$, then there exists a unique $\delta : u \to u'$ in $\Sigma\mathcal{A}$ such that $\delta \cdot t = T(s(\delta))t = t'$ and $\bar{x}'(s(\delta)) = \bar{x}$. Hence, $T(\bar{x})t = T(\bar{x}')T(s(\delta))t = T(\bar{x}')t'$.

For injectivity, assume that there exists $t \underset{\bar{u}}{\otimes} \bar{x}$ and $t' \underset{\bar{u}}{\otimes} \bar{x}'$ in $\widetilde{\mathrm{Tr}}T(X, b)$ such that $T(\bar{x})t = T(\bar{x}')t'$. Since $t$ is generic, there exists a unique $f : s(u) \to s(u')$ such that $\bar{x}'f = \bar{x}$ and $T(f)t = t'$. Likewise, since $t'$ is generic, there exists a unique $h : s(u') \to s(u)$ such that $\bar{x}h = \bar{x}'$ and $T(h)t' = t$. Using again the genericity of $t$ and $t'$, we obtain that $fh = \text{id}$ and $hf = \text{id}$. Hence, by Lemma 8.17, there exists $\alpha : u \to u'$ in $\Sigma\mathcal{A}$ such that $f \cong s\alpha$ which implies that $t \underset{\bar{u}}{\otimes} \bar{x} = t \underset{\bar{u}}{\otimes} \bar{x}'(s\alpha) = \alpha \cdot t \underset{\bar{u}}{\otimes} \bar{x}' = t' \underset{\bar{u}}{\otimes} \bar{x}'$ as desired.

For surjectivity, let $t : b \to T(X)$ be a morphism in $\mathcal{S}(\mathcal{B})$. By Lemma 8.18, there exists $u \in \Sigma\mathcal{A}$, $g : b \to T(s(u))$ generic and $\bar{x} : s(u) \to X$ such that $t = T(\bar{x})g$. Hence, $t \underset{\bar{u}}{\otimes} g \in \widetilde{\mathrm{Tr}}T(X, b)$ is a preimage for $t$. $\square$

**8.2. Cartesian natural transformations.** Our purpose now is to extend this result to a bicategorical equivalence, which we achieve by investigating the correspondence at the level of natural transformations.

The situation at this level has subtle ramifications already in the setting of Berry's domain theory: for cpos $A$ and $B$ the pointwise order on the set of stable functions does not lead to a cartesian closed category. Indeed, to obtain cartesian closure one is forced to restrict the objects to cpos with bounded meets, and the stable function space $A \Rightarrow B$ must be ordered according to

$$ f \sqsubseteq_{\mathrm{st}} g \iff \forall x \leq_A y \in A. g(x) \wedge f(y) = f(x). $$

By considering $x \leq_A x$ in $A$, one necessarily has that $f(x) \leq_B g(x)$, so this is a strengthening of the pointwise order. In fact the order $\sqsubseteq_{\mathrm{st}}$ is precisely what is needed to characterize inclusion at the level of traces, and it is via a categorification of this order that we will establish our correspondence result.
The appropriate notion is that of cartesian natural transformations, whose naturality squares are pullbacks. These generalize the order $\sqsubseteq_{\text{st}}$ on stable functions (consider the naturality square for $x \leq_A y$), and additionally preserve and reflect generic morphisms [Web04]. Cartesian natural transformations are considered also in the settings of normal functors and polynomial functors [Gir88, GK13]. With the interpretation of polynomial functors as arising from sets of operations with arities, a cartesian natural transformation corresponds to a mapping between operations that preserves arities.

We show in this section that our construction yields a biequivalence between the bicategory of stable species and the 2-category **Stable** defined below:

**Definition 8.20.** The 2-category **Stable** has Boolean kits as objects, stable functors $\mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$ as morphisms $\mathcal{A} \to \mathcal{B}$, and cartesian natural transformations as 2-cells.

Natural transformations between stable species in **SEsp** yield cartesian transformations between the corresponding stable functors.

**Proposition 8.21.** Let $(\mathcal{A}, \mathcal{A})$, $(\mathcal{B}, \mathcal{B})$ be Boolean kits and let $f : \mathcal{P} \Rightarrow \mathcal{Q}$ be a natural transformation between stable species $\mathcal{P}, \mathcal{Q} : \Sigma(\mathcal{A}, \mathcal{A}) \to (\mathcal{B}, \mathcal{B})$. The natural transformation $\tilde{f} : \tilde{\mathcal{P}} \Rightarrow \tilde{\mathcal{Q}} : \tilde{\mathcal{S}}(\mathcal{A}, \mathcal{A}) \to \tilde{\mathcal{S}}(\mathcal{B}, \mathcal{B})$, canonically induced by left Kan extension, is cartesian.

*Proof.* Let $g : X \to Y$ in $\mathcal{S}(\mathcal{A})$, we want to show that the square below is a pullback in **Set** for all $b \in \mathcal{B}$:

$$ \begin{array}{ccc} \tilde{P}(X)(b) & \xrightarrow{\tilde{f}_X} & \tilde{Q}(X)(b) \\ \bigdownarrow & & \bigdownarrow \\ \tilde{P}(g) & & \tilde{Q}(g) \\ \bigdownarrow & & \bigdownarrow \\ \tilde{P}(Y)(b) & \xrightarrow{\tilde{f}_Y} & \tilde{Q}(Y)(b) \end{array} $$

We show that for all $(p \underset{\bar{u}_1}{\otimes} \bar{y}) \in \tilde{P}(Y)(b)$ and $(q \underset{\bar{u}_2}{\otimes} \bar{x}) \in \tilde{Q}(X)(b)$ such that

$$ f_{u_1}(p) \underset{\bar{u}_1}{\otimes} \bar{x} = \tilde{f}_Y(p \underset{\bar{u}_1}{\otimes} \bar{x}) = \tilde{Q}(g)(q \underset{\bar{u}_2}{\otimes} \bar{x}) = q \underset{\bar{u}_2}{\otimes} g(\bar{x}) $$

there exists a unique $t \in \tilde{P}(X)(b)$ such that $\tilde{P}(g)(t) = p \underset{\bar{u}_1}{\otimes} \bar{y}$ and $\tilde{f}_X(t) = q \underset{\bar{u}_2}{\otimes} \bar{x}$. The equality $f_{u_1}(p) \underset{\bar{u}_1}{\otimes} \bar{y} = q \underset{\bar{u}_2}{\otimes} g(\bar{x})$ implies that there exists $\alpha : u_1 \to u_2$ in $\Sigma\mathcal{A}$ such that $q = \alpha \cdot f(p)$ and $g(\bar{x}) \cdot \alpha = g(\bar{x}) \circ s(\alpha) = \bar{y}$. Define $t$ to be $p \underset{\bar{u}_1}{\otimes} (\bar{x} \cdot \alpha) \in \tilde{P}(X)(b)$, we then obtain that

$$ \tilde{P}(g)(t) = p \underset{\bar{u}_1}{\otimes} g(\bar{x} \cdot \alpha) = p \underset{\bar{u}_1}{\otimes} g(\bar{x}) \cdot \alpha = p \underset{\bar{u}_1}{\otimes} \bar{y} $$

and

$$ \tilde{f}_X(t) = f(p) \underset{\bar{u}_1}{\otimes} \bar{x} \cdot \alpha = \alpha \cdot f(p) \underset{\bar{u}_2}{\otimes} \bar{x} = q \underset{\bar{u}_2}{\otimes} \bar{x}. $$

Assume now that there exists $v = p_0 \underset{\bar{u}_0}{\otimes} \bar{x}_0 \in \tilde{P}(X)(b)$ such that $\tilde{P}(g)(v) = p \underset{\bar{u}_1}{\otimes} \bar{y}$ and $\tilde{f}_X(v) = q \underset{\bar{u}_2}{\otimes} \bar{x}$. We then have that $p_0 \underset{\bar{u}_0}{\otimes} g(\bar{x}_0) = p \underset{\bar{u}_1}{\otimes} \bar{y}$ and $f(p_0) \underset{\bar{u}_0}{\otimes} \bar{x}_0 = q \underset{\bar{u}_2}{\otimes} \bar{x}$. Hence, there exists $\beta : u_0 \to u_1$ in $\Sigma\mathcal{A}$ such that $q = f(p_0) \cdot \beta$ and $\bar{x} \cdot \beta = \bar{x}_0$, and there exists $\gamma : u_1 \to u_0$ in $\Sigma\mathcal{A}$ such that $p_0 = \gamma \cdot p$ and $g(\bar{x}_0) \cdot \gamma = \bar{y}$. Therefore,

$$ \beta\gamma \cdot f(p) = \beta \cdot f(\gamma \cdot p) = \beta \cdot f(p_0) = q $$

and

$$ g(\bar{x}) \cdot \beta\gamma = g(\bar{x} \cdot \beta) \cdot \gamma = g(\bar{x}_0) \cdot \gamma = \bar{y}. $$
Therefore, $\beta\gamma\alpha^{-1}$ is in $\text{Stab}(Y^\Sigma(u_1))$ which implies that $\beta\gamma\alpha^{-1} \in \bigcup!\mathcal{A}(u_1)$ since $Y \in \mathcal{S}(\mathcal{A})$. We also have $\beta\gamma\alpha^{-1} \cdot q = q$. Since $Q$ is a stable species and $\text{id}_b$ is in $\bigcup\mathcal{B}^\perp(b)$, we obtain that $\beta\gamma\alpha^{-1}$ is in $\bigcup!\mathcal{A}^\perp(u_1)$ which implies that $\alpha = \beta\gamma$. Hence, we have

$$t = p_{\mathcal{A}_1} (\bar{x} \cdot \beta\gamma) = p_{\mathcal{A}_1} (\bar{x}_0 \cdot \gamma) = (\gamma \cdot p)_{\mathcal{A}_0} \bar{x}_0 = p_0 \mathcal{A}_0 \bar{x}_0 = v$$

as desired.

□

We therefore have that $\tilde{(-)}$ defines a functor $\text{SEsp}(\mathcal{A}, \mathcal{B}) \to \text{Stable}(\mathcal{A}, \mathcal{B})$.

**Lemma 8.22.** Let $(\mathcal{A}, \mathcal{A})$, $(\mathcal{B}, \mathcal{B})$ be Boolean kits and $T, S: \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$ be stable functors. For a cartesian transformation $f: T \Rightarrow S$, the transformation $\text{Tr}(f): \text{Tr}(T) \Rightarrow \text{Tr}(S): \mathcal{A}, \mathcal{A} \to \mathcal{B}, \mathcal{B}$ whose components $\text{Tr}(f)_{(b,u)}: \text{Tr}(T)(b, u) \to \text{Tr}(S)(b, u)$ are given by:

$$(t : b \to T(s(u)) \mapsto (f_{s(u)}(t) : b \to S(s(u))$$

is well-defined and natural.

*Proof.* Since cartesian transformations preserve and reflect generic elements, $f_{s(u)}(t)$ is generic if $t$ is generic. Naturality of $\text{Tr}(f)$ follows immediately from the naturality of $f$. □

**Theorem 8.23.** There is a biequivalence $\text{Stable} \simeq \text{SEsp}$.

*Proof.* We now have an adjoint equivalence $\text{SEsp}(\mathcal{A}, \mathcal{B}) \simeq \text{Stable}(\mathcal{A}, \mathcal{B})$ for Boolean kits $\mathcal{A}$ and $\mathcal{B}$. Indeed, the functors $\tilde{(-)}$ and $\text{Tr}$ are well-defined by Propositions 8.12, 8.21, 8.14 and Lemma 8.22. They form an equivalence by Lemmas 8.15 and 8.19 and since any equivalence induces an adjoint equivalence, we obtain the desired result. □

As a corollary, we obtain that **Stable** is cartesian closed (as a bicategory).

## 9. THE LINEAR DECOMPOSITION OF STABLE FUNCTORS

The linear decomposition of the function space

$$A \Rightarrow B = !A \dashv B$$

in Girard's original coherence space model [Gir86] is what triggered the development of linear logic. With this insight, one can define cartesian closed models starting from models of linear logic, as we have done for stable species using stabilized profunctors.

Unlike stable species, the notion of stable functor does not immediately lead to a linear decomposition as above, but our correspondence theorem (Theorem 8.23) induces the following chain of equivalences:

$$\text{Stable}(\mathcal{A}, \mathcal{B}) \simeq \text{SEsp}(\mathcal{A}, \mathcal{B}) = \text{SProf}(!\mathcal{A}, \mathcal{B}). \qquad (9.1)$$

Below we describe a purely extensional decomposition of the form

$$\text{Stable}(\mathcal{A}, \mathcal{B}) \simeq \text{Linear}(!\mathcal{A}, \mathcal{B})$$

for **Linear** a sub-2-category of **Stable** which we define. This decomposition is derived from (9.1) through a biequivalence $\text{SProf} \simeq \text{Linear}$ analogous to the biequivalence between the bicategory **Prof** and the 2-category **Cocont** in Theorem 3.3. Concretely, this biequivalence is given in the direction $\text{Prof} \to \text{Cocont}$ by the mapping $P \mapsto P^\#$, and in the reverse direction by pre-composition with the Yoneda embedding: for any functor $\mathcal{P}(\mathcal{A}) \to \mathcal{P}(\mathcal{B})$ the composite $\mathcal{A} \hookrightarrow \mathcal{P}(\mathcal{A}) \to \mathcal{P}(\mathcal{B})$ determines a profunctor.
That this is a biequivalence relies on two facts. First, because $\mathcal{Y}$ is an embedding, the 2-cell fitting in the Kan extension diagram

<figure><img src="image_22.png" /></figure>

is an isomorphism. Second, the categories $\mathcal{P}(\mathcal{A})$ and $\mathcal{P}(\mathcal{B})$ are locally small and cocomplete, so that $P^{\#}$ always has a right adjoint $\mathcal{Y} \mapsto (\mathcal{A} \mapsto \mathcal{P}(\mathcal{B})(\mathcal{P}(\mathcal{A}), \mathcal{Y}))$, and for functors $\mathcal{P}(\mathcal{A}) \to \mathcal{P}(\mathcal{B})$ (with $\mathcal{A}$ and $\mathcal{B}$ small) to be cocontinuous and to have a right adjoint are equivalent properties.

The first of these facts extends to **SProf** without difficulty: for kits $\mathcal{A}$ and $\mathcal{B}$ and a stabilized profunctor $P : \mathcal{A} \to \mathcal{B}$, the restriction of $P^{\#}$ to stabilized presheaves coincides with the left Kan extension of $P$ along the restricted Yoneda embedding $\mathcal{Y}_{\mathcal{A}} : \mathcal{A} \to \mathcal{S}(\mathcal{A})$ and indeed we have $P^{\#} \circ \mathcal{Y}_{\mathcal{A}} \cong P$ (Lemma 9.4).

On the other hand, categories of stabilized presheaves do not have all colimits, and the functors $P^{\#} : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$ are not left adjoints in general. They do however have a right adjoint on each slice, and this property suffices to characterize them among the stable functors.

**Definition 9.1.** For kits $\mathcal{A}$ and $\mathcal{B}$, a functor $L : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$ is called *linear* if it is stable and a local left adjoint.

Local left adjoints do not preserve all colimits, but for a linear functor $L : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$ the following weaker property holds: for a diagram $D : J \to \mathcal{S}(\mathcal{A})$, if $\mathrm{colim}_{j \in J} D_j$ exists in $\mathcal{S}(\mathcal{A})$, and $\mathrm{colim}_{j \in J} F(D_j)$ exists in $\mathcal{S}(\mathcal{B})$, then $F(\mathrm{colim}_{j \in J} D_j) = \mathrm{colim}_{j \in J} F(D_j)$. Therefore, in particular, $L$ preserves all sums, and for a group $G \in \mathcal{A}(a)$, $L(y(a|G))$ is the colimit of the diagram

$$G \to \mathcal{A} \hookrightarrow \mathcal{S}(\mathcal{A}) \xrightarrow{L} \mathcal{S}(\mathcal{B}).$$

We call **Linear** the sub-2-category of **Stable** consisting of linear functors and cartesian natural transformations between them, and proceed to construct a biequivalence $\mathcal{SProf} \simeq \mathcal{Linear}$ in several steps.

We first verify that for a stabilized profunctor $P : \mathcal{A} \to \mathcal{B}$, the restriction of $P^{\#}_{\mathcal{A}}$ is isomorphic to the left Kan extension of $P$ along the restricted Yoneda embedding $\mathcal{Y}_{\mathcal{A}} : \mathcal{A} \to \mathcal{S}(\mathcal{A})$ by using the universal property of Kan extensions in terms of weighted colimits:

**Proposition 9.2.** For functors $F : \mathcal{A} \to \mathcal{C}$ and $H : \mathcal{A} \to \mathcal{B}$, there is an isomorphism:

$$\mathcal{C}((\mathrm{Lan}_{H}F)(b)), c) \cong \mathcal{P}\mathcal{A}(\mathcal{B}(H(-), b), \mathcal{C}(F(-), c)).$$

**Lemma 9.3.** Let $I : \mathcal{C} \to \mathcal{D}$ and $J : \mathcal{B} \to \mathcal{E}$ be embeddings. For functors $F : \mathcal{A} \to \mathcal{C}$, $H : \mathcal{A} \to \mathcal{B}$ and $L : \mathcal{B} \to \mathcal{C}$, if $IL \cong (\mathrm{Lan}_{JH}(IF))J$ then $L \cong \mathrm{Lan}_{HF}F$.

<figure><img src="image_23.png" /></figure>
Proof. For all $b \in \mathbb{B}$ and $c \in \mathbb{C}$, we have:

$$ \begin{align*} \mathbb{C}(L(b), c) &\cong \mathbb{D}(IL(b), I(c)) \\ &\cong \mathbb{D}(\mathrm{Lan}_{JH}(IF)(Jb), I(c)) \\ &\cong \mathcal{P}\mathcal{A}(\mathbb{E}(JH(-), J(b)), \mathbb{D}(IF(-), I(c))) \\ &\cong \mathcal{P}\mathcal{A}(\mathbb{B}(H(-), b), \mathbb{C}(F(-), c)) \end{align*} $$

By Proposition 9.2, we obtain the desired result.

<figure><img src="image_24.png" /></figure>

**Lemma 9.4.** Let $\underline{\mathcal{A}} = (\mathcal{A}, \mathcal{A})$ and $\underline{\mathbb{B}} = (\mathbb{B}, \mathcal{A})$ be Boolean kits. For a profunctor $P : \mathcal{A} \dashrightarrow \mathbb{B}$, if the functor $P^{\#}_{\iota_{\mathcal{A}}} : \mathcal{S}(\underline{\mathcal{A}}) \rightarrow \mathcal{P}\mathbb{B}$ factors through $\iota_{\mathbb{B}}$ by a functor $L : \mathcal{S}(\underline{\mathcal{A}}) \rightarrow \mathcal{S}(\underline{\mathbb{B}})$, then there exists a functor $Q : \mathcal{A} \rightarrow \mathcal{S}(\underline{\mathbb{B}})$ such that $P$ factors through $\iota_{\mathbb{B}}$ by $Q$ and $L \cong \mathrm{Lan}_{\mathcal{Y}_{\mathcal{A}}} Q$.

<figure><img src="image_25.png" /></figure>

Proof. The restricted functor $L : \mathcal{S}(\underline{\mathcal{A}}) \rightarrow \mathcal{S}(\underline{\mathbb{B}})$ such that $P^{\#}_{\iota_{\mathcal{A}}} = \iota_{\mathbb{B}}L$ is obtained from Lemma 7.9. Since $y_{\mathcal{A}}$ is fully faithful, we have $P \cong P^{\#}_{y_{\mathcal{A}}} = P^{\#}_{\iota_{\mathcal{A}}y_{\mathcal{A}}} = \iota_{\mathbb{B}}L y_{\mathcal{A}}$. Let $Q := L y_{\mathcal{A}} : \mathcal{A} \rightarrow \mathcal{S}(\underline{\mathbb{B}})$, we obtain that $L \cong \mathrm{Lan}_{\mathcal{Y}_{\mathcal{A}}} Q$ by Lemma 9.3. $\square$

<figure><img src="image_26.png" /></figure>

For a stabilized profunctor $P : \underline{\mathcal{A}} \dashrightarrow \underline{\mathbb{B}}$ we denote by $\bar{P} : \mathcal{S}(\underline{\mathcal{A}}) \rightarrow \mathcal{S}(\underline{\mathbb{B}})$ the functor $\mathrm{Lan}_{\mathcal{Y}_{\mathcal{A}}} P \cong P^{\#}_{\iota_{\mathcal{A}}}$. We proceed to show that $(-)$ induces a functor from $\mathcal{SProf}(\underline{\mathcal{A}}, \underline{\mathbb{B}})$ to $\mathbf{Linear}(\underline{\mathcal{A}}, \underline{\mathbb{B}})$.

**Lemma 9.5.** For Boolean kits $\underline{\mathcal{A}}, \underline{\mathbb{B}}$, a presheaf $X \in \mathcal{S}(\underline{\mathcal{A}})$ and a stabilized profunctor $P : \underline{\mathcal{A}} \dashrightarrow \underline{\mathbb{B}}$, if two elements $p \underset{\underline{\mathcal{A}}}{\boxtimes} x$ and $p' \underset{\underline{\mathcal{A}}}{\boxtimes} x'$ in $P^{\#}X$ are equal, there exists a unique $\alpha : a \rightarrow a'$ in $\mathcal{A}$ such that $x' \cdot f = x$ and $f \cdot p = p'$.

Proof. Similar to Lemma 8.11.

<figure><img src="image_27.png" /></figure>

**Lemma 9.6.** For kits $\underline{\mathcal{A}} = (\mathcal{A}, \mathcal{A})$ and $\underline{\mathbb{B}} = (\mathbb{B}, \mathcal{B})$, if a profunctor $P : \underline{\mathcal{A}} \dashrightarrow \underline{\mathbb{B}}$ is in $\mathcal{SProf}(\underline{\mathcal{A}}, \underline{\mathbb{B}})$, then $\bar{P} : \mathcal{S}(\underline{\mathcal{A}}) \rightarrow \mathcal{S}(\underline{\mathbb{B}})$ is stable.

Proof. Since $P^{\#} : \mathcal{P}\mathcal{A} \rightarrow \mathcal{P}\mathbb{B}$ is cocontinuous by Theorem 3.3 and the embeddings $\iota_{\mathcal{A}} : \mathcal{S}(\underline{\mathcal{A}}) \hookrightarrow \mathcal{P}\mathcal{A}$, $\iota_{\mathbb{B}} : \mathcal{S}(\underline{\mathbb{B}}) \hookrightarrow \mathcal{P}\mathbb{B}$ create filtered colimits and epimorphisms by Corollary 7.12, the functor $\bar{P} \cong P^{\#}_{\iota_{\mathcal{A}}} : \mathcal{S}(\underline{\mathcal{A}}) \rightarrow \mathcal{S}(\underline{\mathbb{B}})$ is finitary and epi-preserving.

It remains to show that $\bar{P}$ admits generic factorizations. By Proposition 8.9, it suffices to show that $\bar{P}$ admits generic factorizations relative to representables. Consider a morphism $yb \rightarrow \bar{P}(X)$ in $\mathcal{S}(\underline{\mathbb{B}})$, it is of the form $p \underset{\underline{\mathcal{A}}}{\boxtimes} x$ with $p \in P(b, a)$ and $x \in X(a)$ for some $a \in \mathcal{A}$. We show that

$$ yb \xrightarrow{p \underset{\underline{\mathcal{A}}}{\boxtimes} \mathrm{id}} \bar{P}(ya) \xrightarrow{\bar{P}(x)} \bar{P}(X) $$

is a generic factorization for $p \underset{\underline{\mathcal{A}}}{\boxtimes} x$. The equality $p \underset{\underline{\mathcal{A}}}{\boxtimes} x = \bar{P}(x)(p \underset{\underline{\mathcal{A}}}{\boxtimes} \mathrm{id})$ is immediate, it remains to prove that $p \underset{\underline{\mathcal{A}}}{\boxtimes} \mathrm{id}$ is generic.

Assume that there exist $Y, Z \in \mathcal{S}(\underline{\mathcal{A}})$ and morphisms $p' \underset{\underline{\mathcal{A}}}{\boxtimes} y' : yb \rightarrow \bar{P}(Y)$ and $f : Y \rightarrow Z, z : ya \rightarrow Z$ such that the following diagram commutes in $\mathcal{S}(\underline{\mathbb{B}})$:
<figure><img src="image_28.png" /></figure>

The equality $\bar{P}(f)(p' \underset{\alpha}{\otimes} y') = p \underset{\alpha}{\otimes} z$ is equivalent to $p' \underset{\alpha}{\otimes} fy' = p \underset{\alpha}{\otimes} z$ which implies by Lemma 9.5 that there exists a unique $\alpha : a \to a'$ in $\mathcal{A}$ such that $(fy') \cdot \alpha = z$ and $\alpha \cdot p = p'$. We then have $\bar{P}(y' \cdot \alpha)(p \underset{\alpha}{\otimes} \text{id}) = p \underset{\alpha}{\otimes} y' \cdot \alpha = \alpha \cdot p \underset{\alpha}{\otimes} y' = p' \underset{\alpha}{\otimes} y'$. It remains to show uniqueness, assume that there exists $y : ya \to Y$ such that $fy = z$ and $\bar{P}(y)(p \underset{\alpha}{\otimes} \text{id}) = p' \underset{\alpha}{\otimes} y'$ i.e. $p \underset{\alpha}{\otimes} y = p' \underset{\alpha}{\otimes} y'$. It implies that there exists $g : a \to a'$ such that $y' \cdot g = y$ and $g \cdot p = p'$. Hence, $(fy') \cdot g = fy = z$ which implies that $\alpha = g$ so that $y = y' \cdot \alpha$ as desired.

<figure><img src="image_29.png" /></figure>

□

**Lemma 9.7.** For kits $\mathcal{A}, \mathcal{B}$ and a stabilized profunctor $P : \mathcal{A} \to \mathcal{B}$, the functor $\bar{P} : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$ is linear.

*Proof.* Since $\bar{P} : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$ is stable by Lemma 9.6, we need to show that for all $X \in \mathcal{S}(\mathcal{A})$, the induced functor $\mathcal{S}(\mathcal{A})/X \to \mathcal{S}(\mathcal{B})/\bar{P}(X)$ has a right adjoint $R_X$. For $f : X' \to X$ in $\mathcal{S}(\mathcal{A})$ and $g : Y \to \bar{P}(X)$ in $\mathcal{S}(\mathcal{B})$, we require the following correspondence:

<figure><img src="image_30.png" /></figure>

Note that since $\bar{P} = \text{Lan}_{Y_A} P$, the following sets are isomorphic:

$$ \begin{aligned} \mathcal{S}(\mathcal{B})(\bar{P}(X'), Y) &\cong \mathcal{P}\mathcal{A}(\mathcal{P}\mathcal{A}(y_{\mathcal{A}}(-), X'), \mathcal{S}(\mathcal{B})(P(-), Y)) \\ &\cong \mathcal{P}\mathcal{A}(X', \mathcal{S}(\mathcal{B})(P(-), Y)). \end{aligned} $$

Hence, the left triangle commutes in $\mathcal{S}(\mathcal{B})$ if and only if the following square commutes in $\mathcal{P}\mathcal{A}$:

<figure><img src="image_31.png" /></figure>
Let $R_X(Y)$ be given by the following pullback:

$$ \begin{array}{ccc} R_X(Y) & \longrightarrow & \mathcal{S}(\mathbb{B})(P(-), Y) \\ \cline{2-3} R_X(g) & \longrightarrow & \mathcal{S}(\mathbb{B})(P(-), g) \\ X & \longrightarrow & \mathcal{S}(\mathbb{B})(P(-), P^{\#}(X)) \end{array} $$

Explicitly, for $a \in \mathbb{A}$, $R_X(Y)(a)$ is given by:

$$ \{(x, h) \in X(a) \times \mathcal{S}(\mathbb{B})(P(a), Y) \mid \forall b \in \mathbb{B}, \forall p \in P(b, a), p \not\llcorner a = ghp\} $$

and $R_X(g)(x, h) = x$. We check that the presheaf $R_X(Y)$ is in $\mathcal{S}(\mathbb{A})$. For $(x, h) \in R_X(Y)(a)$ and $\alpha \in \mathrm{Endo}(a)$, since $(x, h) \cdot \alpha = (x \cdot \alpha, h \circ P(\alpha))$, if $(x, h) \cdot \alpha = (x, h)$ then $x \cdot \alpha = x$ and therefore that $\alpha \in \bigcup \mathcal{A}(a)$. $\square$

At the 2-cell level, we show that the $\overline{(-)}$ operator induces cartesian transformations:

**Lemma 9.8.** For Boolean kits $\mathbb{A}, \mathbb{B}$ and a natural transformation $f$ in $\mathcal{SProf}(P, Q)$, the natural transformation $\bar{f} : \bar{P} \Rightarrow \bar{Q} : \mathcal{S}(\mathbb{A}) \to \mathcal{S}(\mathbb{B})$ is cartesian.

*Proof.* Let $h : X \to Y$ in $\mathcal{S}(\mathbb{A})$, we want to show that the square below is a pullback in **Set** for all $b \in \mathbb{B}$.

$$ \begin{array}{ccc} \bar{P}(X)(b) & \xrightarrow{\bar{f}_X} & \bar{Q}(X)(b) \\ \bar{P}(h) & \bigdownarrow & \bar{Q}(h) \\ \bar{P}(Y)(b) & \xrightarrow{\bar{f}_Y} & \bar{Q}(Y)(b) \end{array} $$

We show that for all $(p \not\llcorner a_1, y) \in \bar{P}(Y)(b)$ and $(q \not\llcorner a_2, x) \in \bar{Q}(X)(b)$ such that

$$ f(p) \not\llcorner a_1 = \bar{f}_Y(p \not\llcorner a_1, x) = \bar{Q}(h)(q \not\llcorner a_2, x) = q \not\llcorner a_2 h(x) $$

there exists a unique $u \in \bar{P}(X)(b)$ such that $\bar{P}(h)(u) = p \not\llcorner a_1, y$ and $\bar{f}_X(u) = q \not\llcorner a_2, x$. The equality $f(p) \not\llcorner a_1 = q \not\llcorner a_2, h(x)$ implies that there exists $\alpha : a_1 \to a_2$ in $\mathbb{A}$ such that $q = \alpha \cdot f(p)$ and $h(x) \cdot \alpha = y$. Define $u$ to be $p \not\llcorner a_1 (x \cdot \alpha) \in \bar{P}(X)(b)$, we then obtain that

$$ \bar{P}(h)(u) = p \not\llcorner a_1 h(x \cdot \alpha) = p \not\llcorner a_1 h(x) \cdot \alpha = p \not\llcorner a_1 y $$

and

$$ \bar{f}_X(u) = f(p) \not\llcorner a_1, x \cdot \alpha = \alpha \cdot f(p) \not\llcorner a_2, x = q \not\llcorner a_2, x. $$

Assume now that there exists $v = p_0 \not\llcorner a_0, x_0 \in \bar{P}(X)(b)$ such that $\bar{P}(h)(v) = p \not\llcorner a_1, y$ and $\bar{f}_X(v) = q \not\llcorner a_2, x$. We then have that $p_0 \not\llcorner a_0, h(x_0) = p \not\llcorner a_1, y$ and $f(p_0) \not\llcorner a_0, x_0 = q \not\llcorner a_2, x$. Hence, there exists $\beta : a_0 \to a_1$ in $\mathbb{A}$ such that $q = f(p_0) \cdot \beta$ and $x \cdot \beta = x_0$, and there exists $\gamma : a_1 \to a_0$ in $\mathbb{A}$ such that $p_0 = \gamma \cdot p$ and $h(x_0) \cdot \gamma = y$. Therefore,

$$ \beta\gamma \cdot f(p) = \beta \cdot f(\gamma \cdot p) = \beta \cdot f(p_0) = q \quad \text{and} \quad h(x) \cdot \beta\gamma = h(x \cdot \beta) \cdot \gamma = h(x_0) \cdot \gamma = y. $$

Therefore, $\beta\gamma\alpha^{-1}$ is in $\mathrm{Stab}(Y(a_1))$ which implies that $\beta\gamma\alpha^{-1} \in \bigcup \mathcal{A}(a_1)$. We also have $\beta\gamma\alpha^{-1} \cdot q = q$. Since $Q$ is a stabilized profunctor and $\mathrm{id}_b$ is in $\bigcup \mathcal{B}^{\perp}(b)$, we obtain that $\beta\gamma\alpha^{-1}$ is in $\bigcup \mathcal{A}^{\perp}(a)$ which implies that $\alpha = \beta\gamma$. Hence, we have

$$ u = p \not\llcorner a_1 (x \cdot \beta\gamma) = p \not\llcorner a_1 (x_0 \cdot \gamma) = (\gamma \cdot p) \not\llcorner a_0, x_0 = p_0 \not\llcorner a_0, x_0 = v $$
as desired.

□

For the reverse direction, we define a linear trace operator **tr** : **Linear**($\mathbb{A}$, $\mathbb{B}$) → **SProf**($\mathbb{A}$, $\mathbb{B}$) mapping $L \mapsto Ly_A$ for a linear functor $L : \mathcal{S}(\mathbb{A}) \to \mathcal{S}(\mathbb{B})$. We proceed to show that **tr** is a well-defined functor.

**Lemma 9.9.** Let $\mathbb{A} = (\mathbb{A}, \mathcal{A})$, $\mathbb{B} = (\mathbb{B}, \mathcal{B})$ be Boolean kits and $L : \mathcal{S}(\mathbb{A}) \to \mathcal{S}(\mathbb{B})$ a linear functor. For every $X$ in $\mathcal{S}(\mathbb{A})$ and $l : b \to L(X)$ in $\mathcal{S}(\mathbb{B})$, there exists $a \in \mathbb{A}$, $g : b \to L(y_{\mathbb{A}}(a))$ generic and $x : y_{\mathbb{A}}(a) \to X$ such that $l = L(x)g$.

*Proof.* Since $L$ is linear, $l$ can be factored as $b \xrightarrow{g} L(Y) \xrightarrow{L(f)} L(X)$ where $g$ is generic. By Corollary 7.6, $Y \cong \bigsqcup_{i \in I} y(a_i|G_i)$ where each $G_i$ is a finitely generated group in $\mathcal{A}(a_i)$. Since $L$ preserves coproducts, we obtain that $L(Y) \cong \bigsqcup_{i \in I} L(y(a_i|G_i))$.

Since colimits are computed pointwise in $\mathcal{S}(\mathbb{B})$, it implies that there exists $a$ and $G$ such that $g$ can be factored as

$$b \xrightarrow{g'} L(y(a|G)) \xrightarrow{L(\mathrm{inj})} \bigsqcup_{i \in I} L(y(a_i|G_i)).$$

Since $y(a|G)$ is the colimit of $(g : y_{\mathbb{A}}(a) \to y_{\mathbb{A}}(a))_{g \in G}$ in $\mathcal{S}(\mathbb{A})$ and $L$ is linear, $L(y(a|G))$ is the colimit of $(L(g) : L(y_{\mathbb{A}}(a)) \to L(y_{\mathbb{A}}(a)))_{g \in G}$ in $\mathcal{S}(\mathbb{B})$. Hence, there exists $g'' : b \to L(y_{\mathbb{A}}(a))$ such that $L(q)g'' = g'$.

Since $g$ is generic, there exists $h : Y \to y_{\mathbb{A}}(a)$ such that $\mathrm{inj} \circ q \circ h = \mathrm{id}$ and $L(h)g = g''$ where $q : y_{\mathbb{A}}(a) \to y(a|G)$ is the quotient map.

$$ \begin{tikzcd} & & b \arrow[d, "g'"'] \arrow[r, "g"] & L(y_{\mathbb{A}}(a)) \\ & g & L(h) & L(\mathrm{inj} \circ q) \\ L(Y) & \arrow[r, "L(id)"'] & L(Y) & \arrow[d, "g''"'] \arrow[d, "L(Y)"] \arrow[r, "L(Y)", "L(inj)"'] & L(y_{\mathbb{A}}(a)) \end{tikzcd} $$

Since $h$ is split monic, by Lemma 8.16, $Y$ is isomorphic to $y_{\mathbb{A}}(a)$.

□

**Corollary 9.10.** For Boolean kits $\mathbb{A} = (\mathbb{A}, \mathcal{A})$ and $\mathbb{B} = (\mathbb{B}, \mathcal{B})$, if a functor $L : \mathcal{S}(\mathbb{A}) \to \mathcal{S}(\mathbb{B})$ is linear, then for every $l : b \to L(y_{\mathbb{A}}(a))$ in $\mathcal{S}(\mathbb{B})$, $l$ is generic.

*Proof.* By Lemma 9.9, there exists $g : b \to L(y_{\mathbb{A}}(a_0))$ generic and $\alpha : y_{\mathbb{A}}(a_0) \to y_{\mathbb{A}}(a)$ such that $l = L(\alpha)g$. Since $\alpha$ is an isomorphism, we obtain that $l$ is generic as well.

□

**Lemma 9.11.** For Boolean kits $\mathbb{A} = (\mathbb{A}, \mathcal{A})$ and $\mathbb{B} = (\mathbb{B}, \mathcal{B})$, if a functor $L : \mathcal{S}(\mathbb{A}) \to \mathcal{S}(\mathbb{B})$ is linear then $\mathrm{tr}(L) : \mathbb{A} \dashrightarrow \mathbb{B}$ given by $Ly_{\mathbb{A}}$ is a stabilized profunctor.

*Proof.* Let $l : b \to L(y_{\mathbb{A}}(a))$ be in $\mathrm{tr}(L)(b, a)$ and $\alpha \in \mathbb{A}(a, a)$, $\beta \in \mathbb{B}(b, b)$ such that $\alpha \cdot l \cdot \beta = l$, i.e. the following square commutes in $\mathcal{S}(\mathbb{B})$:

$$ \begin{tikzcd} & & b \arrow[d, "l"'] \arrow[r, "b"'] & L(y_{\mathbb{A}}(a)) \\ \beta & & & L(y_{\mathbb{A}}\alpha) \\ & b & L(y_{\mathbb{A}}(a)) & \arrow[d, "l"'] \arrow[r, "b"'] \arrow[d, "L(Y)"] \arrow[r, "L(Y)", "L(inj)"'] & L(y_{\mathbb{A}}(a)) \end{tikzcd} $$
Assume that $\alpha \in \bigcup \mathcal{A}(a)$, then $y(a|\langle\alpha\rangle) \in \mathcal{S}(\mathcal{A})$. Let $q : y_{\mathcal{A}}(a) \to y(a|\langle\alpha\rangle)$ be the quotient map, we then have that $q \circ y_{\mathcal{A}}(\alpha) = q$ in $\mathcal{S}(\mathcal{A})$ which implies that the following diagram commutes in $\mathcal{S}(\mathcal{B})$:

<figure><img src="image_32.png" /></figure>

Hence, $\beta \in \mathrm{Stab}(L(q)l)$ which implies that $\beta \in \bigcup \mathcal{B}(b)$.

Assume now that $\beta \in \bigcup \mathcal{B}^{\perp}(b)$, we want to show that for all $n$, if $\alpha^n$ is in $\bigcup \mathcal{A}(a)$, then $\alpha^n = \mathrm{id}_a$. If $\alpha^n \in \bigcup \mathcal{A}(a)$, then $y(a|\langle\alpha^n\rangle) \in \mathcal{S}(\mathcal{A})$ and the following diagram commutes in $\mathcal{S}(\mathcal{B})$:

<figure><img src="image_33.png" /></figure>

where $q' : y_{\mathcal{A}}(a) \to y(a|\langle\alpha^n\rangle)$ is the quotient map in $\mathcal{S}(\mathcal{A})$. Hence, $\beta^n \in \mathrm{Stab}(L(q')l)$ which implies that $\beta^n = \mathrm{id}_b$ so that the following diagram commutes:

<figure><img src="image_34.png" /></figure>

Since $l$ is generic by Corollary 9.10, we obtain that $\alpha^n = \mathrm{id}_a$ as desired. $\square$

<figure><img src="image_35.png" /></figure>

Since $\mathbf{SProf}(\mathcal{A}, \mathcal{B})$ is a full subcategory of $\mathbf{Prof}(\mathcal{A}, \mathcal{B})$, for a cartesian transformation $f : L \Rightarrow L'$ in $\mathbf{Linear}(\mathcal{A}, \mathcal{B})$, we automatically have $fy_{\mathcal{A}}$ in $\mathbf{SProf}(\mathcal{A}, \mathcal{B})(Ly_{\mathcal{A}}, L', y_{\mathcal{A}})$.

**Lemma 9.12.** For Boolean kits $\mathcal{A} = (\mathcal{A}, \mathcal{A})$, $\mathcal{B} = (\mathcal{B}, \mathcal{B})$ and a stabilized profunctor $P : \mathcal{A} \dashrightarrow \mathcal{B}$, there is an isomorphism $\eta : P \cong \mathrm{tr}\bar{P}$.

*Proof.* Since we are taking a left Kan extension along a fully faithful functor $y_{\mathcal{A}}$, $P$ is isomorphic to $(\mathrm{Lan}_{y_{\mathcal{A}}} P)y_{\mathcal{A}} = \mathrm{tr}\bar{P}$. $\square$

<figure><img src="image_36.png" /></figure>

**Lemma 9.13.** For Boolean kits $\mathcal{A}$, $\mathcal{B}$ and a linear functor $L : \mathcal{S}(\mathcal{A}) \to \mathcal{S}(\mathcal{B})$, there is an isomorphism $\varepsilon : \overline{\mathrm{tr}(L)} \cong L$.

*Proof.* Let $X$ be in $\mathcal{S}(\mathcal{A})$ and $b \in \mathcal{B}$. An element of $\overline{\mathrm{tr}(L)}(X)(b)$ is of the form $l \underset{\alpha}{\boxtimes} x$ where $l : b \to L(y_{\mathcal{A}}(a))$ and $x \in X(a)$, we define $\varepsilon_{X,b} : \overline{\mathrm{tr}(L)}(X, b) \to L(X, b)$ by $l \underset{\alpha}{\boxtimes} x \mapsto L(x)l$. For $l \underset{\alpha}{\boxtimes} x$ and $l' \underset{\alpha}{\boxtimes} x'$ in $\overline{\mathrm{tr}(L)}(X)(b)$, $l \underset{\alpha}{\boxtimes} x = l' \underset{\alpha}{\boxtimes} x'$ is equivalent to the existence of a unique
$\alpha : a \to a'$ such that $x' \cdot \alpha = x$ and $L(\alpha)l = l'$ which implies that $\varepsilon_{X,b}$ is well-defined and injective. Let $l : b \to L(X)$ be in $\mathcal{S}(\mathbb{B})$, by Lemma 9.9, there exists $a \in \mathbb{A}$, $g : b \to L(y_{\mathcal{A}}(a))$ generic and $x : y_{\mathcal{A}}(a) \to X$ such that $l = L(x)g$. Now, $\varepsilon_{X,b}(g \otimes x) = L(x)g$ which implies that $\varepsilon_{X,b}$ is surjective as desired. Naturality of $\varepsilon$ follows immediately from the functoriality of $L$. $\square$

**Theorem 9.14.** For Boolean kits $\mathbb{A} = (\mathbb{A}, \mathcal{A})$ and $\mathbb{B} = (\mathbb{B}, \mathcal{B})$, there is an adjoint equivalence as follows

$$ \mathbf{SProf}(\mathbb{A}, \mathbb{B}) \xrightarrow{\overline{(-)}} \mathbf{Linear}(\mathbb{A}, \mathbb{B}) \xleftarrow{\perp} \mathbf{tr} $$

*Proof.* The functors $\overline{(-)}$ and $\mathbf{tr}$ are well-defined by Lemmas 9.7, 9.8 and 9.11. They form an equivalence by Lemmas 9.12 and 9.13 and since any equivalence induces an adjoint equivalence, we obtain the desired result. $\square$

We complete the picture by observing that the intensional/extensional biequivalences that we have shown at the linear and stable levels are compatible, with the overall situation summarized in the following diagram

<figure><img src="image_37.png" /></figure>

which is seen to commute up to natural isomorphism.

It is compelling that standard computational intuitions for linearity, involving resource usage, remain accessible in this setting. One has for instance that for a linear functor $L : \mathcal{S}(\mathbb{A}) \to \mathcal{S}(\mathbb{B})$, the trace $\mathbf{Tr}(L) \in \mathbf{SEsp}(\mathbb{A}, \mathbb{B})$ has components

$$ \mathbf{Tr}(L)(b, \langle a_i \rangle_{i \in [n]}) = \begin{cases} \emptyset & \text{if } n \neq 1 \\ L(y(a))(b) & \text{if } \langle a_i \rangle_{i \in [n]} = \langle a \rangle \end{cases} $$

i.e. the result of the computation is determined by inspecting the 'argument' $\mathbb{A}$ exactly once, in accordance with the original ideas of Girard [Gir86].

## 10. CONCLUSION

We have introduced a new bicategorical model of classical linear logic based on groupoids with kits and stabilized profunctors. We have also presented this model in extensional form, in terms of stable functors between subcategories of presheaves. Restricted to discrete groupoids
(i.e. sets), stable functors coincide with finitary polynomial functors $\mathbf{Set}^I \to \mathbf{Set}^J$ between categories of indexed sets, called normal functors in the influential work of Girard [Gir88]. The construction of a cartesian closed bicategory that embeds finitary polynomial functors is a key contribution of this work.

Some aspects of our construction should be understood more abstractly. The bicategory of stable species of structures refines the bicategory of generalized species [FGHW08] by means of an orthogonality construction. Refinements of this kind are well-studied in the 1-categorical setting and provide a rich family of models for linear logic [HS03]. Our construction provides a new example of orthogonality and double-glueing in a two-dimensional setting. The full theory will be developed using the present work as a guiding example.

The notion of kit also deserves further exploration. In particular, various families of non-Boolean kits with additional closure conditions provide models of intuitionistic linear logic. It seems less clear how to understand these models in extensional form.

Finally we mention some related work. Generalized analytic and polynomial functors are considered in the work of Garner and Hirschowitz [GH18], including a method for controlling actions in terms of stabilizers. We will investigate the connections to our work. In a separate line of work, Finster, Lucas, Mimram and Seiller [FMLS21] present another groupoid model, described in the language of homotopy type theory. The relationship with our model should be explored, also in connection to the work of Kock et al. [Koc12, GHK21].

## REFERENCES

[AAG05] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. *Theor. Comput. Sci.*, 342(1):3–27, 2005. doi:10.1016/j.tcs.2005.06.002.

[AGH$^{+}$15] Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride, and Peter Morris. Indexed containers. *J. Funct. Program.*, 25, 2015. doi:10.1017/S095679681500009X.

[ALS10] Thorsten Altenkirch, Paul Blain Levy, and Sam Staton. Higher-order containers. In Fernando Ferreira, Benedikt Löwe, Elvira Mayordomo, and Luís Mendes Gomes, editors, *Programs, Proofs, Processes, 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 - July 4, 2010. Proceedings*, volume 6158 of Lecture Notes in Computer Science, pages 11–20. Springer, 2010. doi:10.1007/978-3-642-13962-8\_2.

[Bar06] Michael Barr. *-*Autonomous categories*, volume 752. Springer, 2006.

[Bén67] Jean Bénabou. Introduction to bicategories. In *Reports of the Midwest Category Seminar*, pages 1–77, Berlin, Heidelberg, 1967. Springer Berlin Heidelberg.

[Bén00] Jean Bénabou. Distributors at work, 2000. Lecture notes written by Thomas Streicher. URL: https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.

[Ber78] Gérard Berry. Stable models of typed lambda-calculi. In *Proceedings of the Fifth Colloquium on Automata, Languages and Programming*, pages 72–89, Berlin, Heidelberg, 1978. Springer-Verlag.

[BLL98] F. Bergeron, G. Labelle, and P. Leroux. *Combinatorial species and tree-like structures*, volume 67 of *Encyclopedia of Mathematics and its Applications*. Cambridge University Press, Cambridge, 1998.

[CJ95] Aurelio Carboni and Peter Johnstone. Connected limits, familial representability and artin glueing. *Mathematical Structures in Computer Science*, 5(4):441–459, 1995. doi:10.1017/S0960129500001183.

[CS97] J Robin B Cockett and Robert AG Seely. Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. *Theory and Applications of categories*, 3(5):85–131, 1997.

[DE11] Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. *Information and Computation*, 209(6):966–991, 2011. URL: http://www.sciencedirect.com/science/article/pii/S0890540111000411, doi: https://doi.org/10.1016/j.ic.2011.02.001.

[Die77] Yves Diers. *Catégories localisables*. PhD thesis, Paris 6 et Centre universitaire de Valenciennes et du Hainaut Cambrésis, 1977.
[Ehr05] Thomas Ehrhard. Finiteness spaces. *Mathematical Structures in Computer Science*, 15(4):615–646, 2005. doi:10.1017/S0960129504004645.

[Ehr18] Thomas Ehrhard. An introduction to differential linear logic: Proof-nets, models and an-tiderivatives. *Mathematical Structures in Computer Science*, 28:995–1060, 2018. doi:10.1017/S0960129516000372.

[ER03] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. *Theoretical Computer Science*, 309(1-3):1–41, 2003.

[FGHW08] Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. *J. Lond. Math. Soc. (2)*, 77(1):203–220, 2008. URL: http://dx.doi.org/10.1112/jlms/jdm096, doi:10.1112/jlms/jdm096.

[FGHW18] Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. *Selecta Mathematica*, 24(3):2791–2830, 2018. doi:10.1007/s00029-017-0361-3.

[FGP22] Marcelo Fiore, Zeinab Galal, and Hugo Paquet. A combinatorial approach to higher-order structure for polynomial functors. In *7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)*. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022.

[Fio05] Marcelo Fiore. Mathematical models of computational and combinatorial structures. In *International Conference on Foundations of Software Science and Computation Structures*, pages 25–46. Springer, 2005.

[Fio07] Marcelo Fiore. Differential structure in models of multiplicative biadditive intuitionistic linear logic. In Simona Ronchi Della Rocca, editor, *Typed Lambda Calculi and Applications*, pages 163–177. Springer, 2007.

[Fio14] Marcelo Fiore. Analytic functors between presheaf categories over groupoids. *Theor. Comput. Sci.*, 546:120–131, 2014. doi:10.1016/j.tcs.2014.03.004.

[FMLS21] Eric Finster, Samuel Mimram, Maxime Lucas, and Thomas Seiller. A cartesian bicategory of polynomial functors in homotopy type theory. In Ana Sokolova, editor, *Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021*, volume 351 of *EPTCS*, pages 67–83, 2021. doi:10.4204/EPTCS.351.5.

[GH18] Richard Garner and Tom Hirschowitz. Shapely monads and analytic functors. *J. Log. Comput.*, 28(1):33–83, 2018. URL: https://doi.org/10.1093/logcom/exx029.

[GHK21] David Gepner, Rune Haugseng, and Joachim Kock. ∞-Operads as analytic monads. *International Mathematics Research Notices*, 2021. doi:10.1093/imrn/rnaa332.

[Gir86] Jean-Yves Girard. The System *F* of variable types, fifteen years later. *Theoretical Computer Science*, 45:159–192, 1986. URL: http://www.sciencedirect.com/science/article/pii/0304397586900447, doi:https://doi.org/10.1016/0304-3975(86)90044-7.

[Gir87] Jean-Yves Girard. Linear logic. *Theor. Comput. Sci.*, 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.

[Gir88] Jean-Yves Girard. Normal functors, power series and λ-calculus. *Ann. Pure Appl. Logic*, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5.

[GK13] Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. *Mathematical Proceedings of the Cambridge Philosophical Society*, 154(1):153–192, 2013. doi:10.1017/S0305004112000394.

[Has02] Ryu Hasegawa. Two applications of analytic functors. *Theoretical Computer Science*, 272(1):113–175, 2002. doi:https://doi.org/10.1016/S0304-3975(00)00349-2.

[HS03] Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. *Theoretical Computer Science*, 294(1):183–231, 2003. doi:https://doi.org/10.1016/S0304-3975(01)00241-9.

[Joy81] André Joyal. Une théorie combinatoire des séries formelles. *Adv. in Math.*, 42(1):1–82, 1981. URL: http://dx.doi.org/10.1016/0001-8708(81)90052-9, doi:10.1016/0001-8708(81)90052-9.

[Joy86] André Joyal. Foncteurs analytiques et espèces de structures. In Gilbert Labelle and Pierre Leroux, editors, *Combinatoire énumérative*, pages 126–159, Berlin, Heidelberg, 1986. Springer Berlin Heidelberg.
[Ker18] Marie Kerjean. A logical account for linear partial differential equations. In Anuj Dawar and Erich Grädel, editors, *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018*, Oxford, UK, July 09-12, 2018, pages 589–598. ACM, 2018. doi:10.1145/3209108.3209192.

[KL19] Marie Kerjean and Jean-Simon Pacaud Lemay. Higher-order distributions for differential linear logic. In Mikolaj Bojanczyk and Alex Simpson, editors, *Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings*, volume 11425 of *Lecture Notes in Computer Science*, pages 330–347. Springer, 2019. doi:10.1007/978-3-030-17127-8\_19.

[Koc12] Joachim Kock. Data types with symmetries and polynomial functors over groupoids. *Electronic Notes in Theoretical Computer Science*, 286:351–365, 2012. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). doi:https://doi.org/10.1016/j.entcs.2013.01.001.

[Lam88] François Lamarche. *Modelling polymorphism with categories*. PhD thesis, McGill University, 1988.

[Law73] F. William Lawvere. Metric spaces, generalized logic, and closed categories. *Rendiconti del Seminario Matematico e Fisico di Milano*, 43:135–166, 1973. Republished in: *Reprints in Theory and Applications of Categories*, No. 1 (2002) pp 1–37.

[Loa94] Ralph Loader. Linear logic, totality and full completeness. In *In Proceedings of LiCS '94*, pages 292–298. Press, 1994.

[LV88] P. Leroux and G.X. Viennot. Combinatorial resolution of systems of differential equations. IV. Separation of variables. *Discrete Mathematics*, 72(1-3):237–250, 1988. doi:10.1016/0012-365X(88)90213-0.

[Oli21] Federico Olimpieri. Intersection type distributors. In *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–15. IEEE, 2021.

[Osm20] Axel Osmond. On Diers theory of Spectrum I : Stable functors and right multi-adjoints, 2020. arXiv:2012.00853.

[Sco76] Dana Scott. Data types as lattices. *SIAM Journal on Computing*, 5:522–587, 09 1976. doi:10.1137/0205037.

[Sta16] Michael Stay. Compact closed bicategories. *Theory and Applications of Categories*, 31(26):755–798, 2016.

[TAO17] Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Generalised species of rigid resource terms. In *2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–12. IEEE, 2017.

[TAO18] Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Species, profunctors and Taylor expansion weighted by smcc: A unified framework for modelling nondeterministic, probabilistic and quantum programs. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '18, pages 889–898, New York, NY, USA, 2018. ACM. URL: http://doi.acm.org/10.1145/3209108.3209157, doi:10.1145/3209108.3209157.

[Tay89] Paul Taylor. Quantitative domains, groupoids and linear logic. In *Category Theory and Computer Science*, pages 155–181. Springer, 1989.

[Tay90] Paul Taylor. An algebraic approach to stable domains. *Journal of Pure and Applied Algebra*, 64(2):171–203, 1990. doi:https://doi.org/10.1016/0022-4049(90)90156-C.

[Tay98] Paul Taylor. The trace factorisation of stable functors. 1998. URL: https://www.paultaylor.eu/stable/trafsf.pdf.

[Web04] Mark Weber. Generic morphisms, parametric representations and weakly cartesian monads. *Theory and Applications of Categories*, 13(14):191–234, 2004.

[Web07] Mark Weber. Familial 2-functors and parametric right adjoints. *Theory Appl. Categ*, 18(22):665–732, 2007.

[Yon60] Nobuo Yoneda. On Ext and exact sequences. *Journal of the Faculty of Science, Imperial University of Tokyo*, 8:507–576, 1960.