∞-Categorical Models of Linear Logic

Harington, Eliès; Mimram, Samuel

doi:10.4230/LIPIcs.FSCD.2025.23

$\infty$ -Categorical Models of Linear Logic

Eliès Harington

LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau, France Samuel Mimram

LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau, France

Abstract

The notion of categorical model of linear logic is now well studied and established around the notion of linear-non-linear adjunction, which encompasses the earlier notions of Seely categories, Lafont categories and linear categories. These categorical structures have counterparts in the realm of $\infty$ -categories, which can thus be thought of as weak forms of models of linear logic. The goal of this article is to formally introduce them and study their relationships. We show that $\infty$ -linear-non-linear adjunctions still play the role of a unifying notion of model in this setting. Moreover, we provide a sufficient condition for a symmetric monoidal $\infty$ -category to be Lafont. Finally, we illustrate our constructions by providing models: we construct linear-non-linear adjunctions that generalize well-known models in relations (and variants based on profunctors or spans), domains and vector spaces. In particular, we introduce a model based on spectra, a homotopical variant of abelian groups.

Keywords and phrases:

linear logic, linear-non-linear adjunction,

\infty

-category, spectrum

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Linear logic

DOI:

10.4230/LIPIcs.FSCD.2025.23

Event:

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Editors:

Maribel Fernández

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Introduction

Toward higher-dimensional models of linear logic.

The introduction of linear logic [20] was motivated by the study of semantics of $\lambda$ -calculus [21] and many instances of such semantics have been considered for this logic (phase semantics, coherence spaces, domains, game semantics, etc.). In order to structure and unify their study, categorical axiomatizations of what a model of linear logic should be have been proposed: Lafont categories [34], Seely categories [45], linear categories [26] and linear-non-linear adjunctions [7], as well as $*$ -autonomous [45, 5] variants for the classical case, see [11, 41, 38] for surveys on the topic and the relationships between them. More recently, the study of several categorical structures has prompted higher-categorical generalizations of the notion of model: even though those do not form categories, but rather bicategories, we can recognize there variants of the familiar structures that are usually found in models of linear logic. We can for instance name generalized species of structures [16, 14], or polynomial functors [32, 18, 13]. Those have motivated the recent introduction of bicategorical models for (differential) linear logic [15]. More recently, higher-dimensional generalizations of those models, polynomial/analytic functors in particular, have been considered in the settings of $\infty$ -categories [19] and homotopy type theory [23]. Those are a motivation for the introduction of $\infty$ -categorical models of linear logic in this paper.

$\infty$ -categories.

The notion of $\infty$ -category originates in the study of homotopy theory, and it has recently garnered an interest from computer science because of its tight relationship with homotopy type theory [47]. It can be thought of as a generalization of the notion of category where we take higher-dimensional coherences into account: this means that, when introducing a structure, we should ask for isomorphisms instead of equalities, those isomorphisms should satisfy coherences, themselves satisfying further coherences, and so on. Because of this, usual structures (such as the very definition of $\infty$ -category) require specifying an infinite amount of data. There are various formalisms making this idea precise, we consider here the one of quasicategories developed by Joyal [29]. It was considerably expanded by Lurie [35, 36], up to the point that we can nowadays almost work as in the 1-categorical setting, justifying every step by preexisting $\infty$ -categorical results.

$\infty$ -categorical models of linear logic.

In this article, we introduce $\infty$ -categorical variants of the main categorical models of linear logic: linear-non-linear adjunctions, Lafont categories, Seely categories, and linear categories. We also show that, as advocated by Melliès in the 1-categorical setting [38], linear-non-linear adjunctions play a unifying role for those various structures. Although, there is no formal connection (yet) to the syntax of linear logic (in the usual sense of denotational semantics), we consider that those relationships are a good indication that we are considering the relevant structures. This has allowed us to come up with new models of linear logic, which generalize already known 1-categorical ones, but are of a quite different nature and exhibit interesting new phenomena: cocomplete $\infty$ -categories and cocontinuous functors (generalizing complete semilattices), $\infty$ -categories and profunctors (generalizing relations), spectra (generalizing abelian groups).

Plan of the paper.

After recalling basic notions of $\infty$ -categories (Section 1), we introduce and compare the various $\infty$ -categorical generalizations of models of linear logic: linear-non-linear adjunctions, among which Seely and linear categories (Section 2.1), Lafont categories (Section 2.2), and $*$ -autonomous categories (Section 2.3). We then recall 1-categorical models of linear logic: polynomials (Section 3.1), domains (Section 3.2) and modules (Section 3.3). We then construct $\infty$ -categorical generalizations of those models in cocomplete $\infty$ -categories (Section 4) and spectra (Section 5).

1 $\infty$ -categories

We very briefly recall the setting of $\infty$ -categories, in the formalism of quasi-categories [29]. Providing a complete introduction is out of the scope of this paper, and we refer to the foundational books of Lurie [35, 36] for a complete reference. Our main goal here is to provide reference to $\infty$ -categorical generalizations of well-known constructions and properties in the 1-categorical world, which we will use in the following.

Simplicial sets.

Given a natural number $n$ , we write $[n]$ for the partial order $\{0<\ldots<n\}$ . We write $\Delta$ for the category of simplices whose objects are natural numbers and morphisms $f:m\to n$ are monotone functions $f:[m]\to[n]$ . The category $\widehat{\Delta}$ of presheaves over this category has simplicial sets as objects. Given an object $n\in\Delta$ , we write $\Delta^{n}$ for the simplicial set obtained as the image of $n$ under the Yoneda embedding, and $\Lambda^{n}_{k}$ for the $k$ -th horn, which is the simplicial set obtained from $\Delta^{n}$ by removing the $k$ -th face and its top-dimensional cell, with $0\leq k\leq n$ ; an inner horn being a horn with $0<k<n$ . Writing $I:\Delta\to\operatorname{Cat}$ for the functor which to $n$ associates the totally ordered set $[n]$ , any category $\mathcal{C}$ induces a simplicial set, called its nerve, defined by $N(\mathcal{C})=\operatorname{Cat}(I-,\mathcal{C})$ , which will allow considering a 1-category as an $\infty$ -category, which we sometimes leave implicit.

$\infty$ -categories.

An $\infty$ -category $\mathcal{C}$ is a simplicial set such that every inner horn has a filler [35, Def 1.1.2.4] (and $\infty$ -groupoids are defined similarly by requiring that every horn has a filler). It can be thought of as a weak variant of the notion of category where the expected laws, such as associativity, hold only up to coherent higher cells (the 0-cells correspond to the objects and the 1-cell to the morphisms of the category). A functor is a morphism of simplicial sets. Any two $\infty$ -categories $\mathcal{C}$ and $\mathcal{D}$ induce an $\infty$ -category $\operatorname{Fun}(\mathcal{C},\mathcal{D})$ (also denoted $[\mathcal{C},\mathcal{D}]$ ) given by the internal hom in $\widehat{\Delta}$ , whose objects are the functors from $\mathcal{C}$ to $\mathcal{D}$ [35, Prop 1.2.7.3]. The morphisms in this $\infty$ -category are called natural transformations. A functor $F:\mathcal{C}\to\mathcal{D}$ is an equivalence when there is a functor $G:\mathcal{D}\to\mathcal{C}$ and two invertible natural transformations $G\circ F\simeq\operatorname{id}_{\mathcal{C}}$ and $F\circ G\simeq\operatorname{id}_{\mathcal{D}}$ [35, Prop 1.2.4.1]. We write $\operatorname{Cat}$ for the $\infty$ -category of $\infty$ -categories [35, Def 3.0.0.1], and $\mathcal{S}$ for the $\infty$ -category of $\infty$ -groupoids [35, Def 1.2.16.1], which we sometimes refer to as spaces. In the following, we use homotopical as synonymous for “ $\infty$ -categorical”, because of the tight relationships with homotopy theory [44]. In particular, all (co)limits in $\infty$ -categories are homotopy (co)limits [35, Sec 1.2.13].

Adjunctions.

Any two objects $A$ and $B$ of an $\infty$ -category $\mathcal{C}$ induce an $\infty$ -groupoid $\operatorname{Hom}_{\mathcal{C}}(A,B)$ (also noted $\mathcal{C}(A,B)$ ) [35, Prop 1.2.2.3]. An adjunction between two $\infty$ -categories $\mathcal{C}$ and $\mathcal{D}$ consists of functors $F:\mathcal{C}\to\mathcal{D}$ and $G:\mathcal{D}\to\mathcal{C}$ , together with a natural transformation $\eta:\operatorname{id}_{\mathcal{C}}\to G\circ F$ such that for every objects $A,B\in\mathcal{D}$ , the composite morphism is an equivalence of $\infty$ -groupoids [35, Def 5.2.2.7]. Such a natural transformation is called a unit for the adjunction. Adjunctions can equivalently be defined dually purely in terms of counits, or by asking for natural transformations $\eta:\operatorname{id}_{\mathcal{C}}\to G\circ F$ and $\varepsilon:F\circ G\to\operatorname{id}_{\mathcal{D}}$ satisfying the usual zig-zag identities up to homotopy, in which case they are automatically the unit and counit for an adjunction between $F$ and $G$ [37, Tag 02EK].

The existence of adjoint functors is often obtained in the following situation. An $\infty$ -category is accessible when it is the completion under filtered colimits of a small $\infty$ -category [35, Def 5.4.2.1], and presentable when it moreover has small colimits [35, Def 5.5.0.1]. The adjoint functor theorem then states that a functor between presentable $\infty$ -categories is a left adjoint if and only if it preserves colimits [35, Cor 5.5.2.9].

Symmetric monoidal $\infty$ -categories.

We write $\operatorname{Fin}_{\ast}$ for the 1-category where an object is a natural number and a morphism $f:m\to n$ is a function $f:[m]\to[n]$ such that $f(0)=0$ . A symmetric monoidal $\infty$ -category $\mathcal{C}$ is a functor $M:\operatorname{Fin}_{\ast}\to\operatorname{Cat}$ (we simply write $\operatorname{Fin}_{\ast}$ instead of $N(\operatorname{Fin}_{\ast})$ ) such that the canonical map $Mn\to(M1)^{n}$ (given by the cartesian structure of $\operatorname{Cat}$ ) is an equivalence [36, Ex 2.4.2.4]. We should mention that, technically, we use the equivalent formulation as a cocartesian fibration $p:\mathcal{C}^{\otimes}\to\operatorname{Fin}_{\ast}$ satisfying suitable properties [36, Def 2.0.0.7]. The notion of cocartesian fibration generalizes to $\infty$ -categories the traditional notion of Grothendieck opfibration [35, Sec 2.4] and $\mathcal{C}^{\otimes}$ is an $\infty$ -category constructed from $\mathcal{C}$ , whose objects are tuples of objects in $\mathcal{C}$ [36, Cons 2.1.1.7]. The opposite of a symmetric monoidal $\infty$ -category has a canonical structure of symmetric monoidal $\infty$ -category using the equivalence $\textnormal{op}:\operatorname{Cat}\to\operatorname{Cat}$ [36, Rem 2.4.2.7]. A symmetric monoidal $\infty$ -category $\mathcal{C}$ is closed when the functor $A\otimes-:\mathcal{C}\to\mathcal{C}$ admits a right adjoint [36, Def 4.1.1.15], which we generally denote $A\multimap-$ . Given a functor $F:\mathcal{C}\to\mathcal{D}$ between symmetric monoidal $\infty$ -categories, a monoidal structure consists in natural isomorphisms exhibiting the fact that the functor preserves the monoidal structure, see [36, Def 2.1.3.7].

Monads.

A commutative monoid in a monoidal $\infty$ -category $p:\mathcal{C}^{\otimes}\to\operatorname{Fin}_{\ast}$ is a section $m:\operatorname{Fin}_{\ast}\to\mathcal{C}^{\otimes}$ satisfying a suitable condition [36, Def 2.1.3.1]. In particular, a commutative monoid in the $\infty$ -category $\operatorname{Cat}$ is a symmetric monoidal $\infty$ -category [36, Rem 2.4.2.6]. The notion of cocommutative comonoid is defined dually as a commutative monoid in the opposite monoidal $\infty$ -category $\mathcal{C}^{\textnormal{op}}$ . The notion of (non-commutative) monoid can be defined similarly, by taking a variant of the $\infty$ -category $\operatorname{Fin}_{\ast}$ [36, Def 4.1.1.6]. A monad $T$ on an $\infty$ -category $\mathcal{C}$ is a monoid object in the monoidal $\infty$ -category $\operatorname{Fun}(\mathcal{C},\mathcal{C})$ [36, Def 4.7.0.1]. Any adjunction between $\infty$ -categories induces a monad in the expected way [36, Prop 4.7.3.3]. Moreover, any monad $T$ on an $\infty$ -category $\mathcal{C}$ determines an $\infty$ -category $\mathcal{C}^{T}$ of $T$ -algebras [36, Def 4.2.1.13]. The Kleisli $\infty$ -category $\mathcal{C}_{T}$ associated to a monad can be described as the essential image of the free algebra functor $\mathcal{C}\to\mathcal{C}^{T}$ (constructed in [36, Sec 4.2.4]), see [25, Def 4.1].

2 $\infty$ -categorical models of linear logic

The notion of categorical model for the multiplicative fragment of intuitionistic linear logic is clear: it consists of a category ${\mathcal{L}}$ which is symmetric monoidal closed (to model the tensor and linear arrow of linear logic). In order to model additives, the category ${\mathcal{L}}$ should be cartesian (independently of being monoidal). Finally, in order to model exponentials, the category should moreover be equipped with a comonad $\mathop{!}:{\mathcal{L}}\to{\mathcal{L}}$ , the exponential modality, equipped with various coherence isomorphisms satisfying suitable coherence laws. Several axiomatizations of this modality have been proposed in the literature, among which Lafont categories [34], Seely categories [45] and linear categories [26], see [11, 38] for a survey. As for any comonad, an exponential comonad can be decomposed as an adjunction, which can be seen as a particular way of “presenting” the comonad. In particular, we have the two extremal ways of decomposing the comonad as the adjunction with the Kleisli category, and the category of coalgebras of the comonad. The properties that such adjunctions should satisfy can be axiomatized as the linear non-linear (lnl) adjunctions introduced by Benton [7], and those have been advocated as a unifying framework for the models of linear logic by Melliès [38]. Again, we insist on the fact that the adjunction is additional data, all that matters is the comonad it induces. We observe here that the various notions of categorical model are difficult to generalize to $\infty$ -categories, but it is much easier to do so with the associated reformulations as lnl adjunctions, which is the point of view we adopt here. Finally, we investigate $*$ -autonomous $\infty$ -categories, which allow modeling classical linear logic.

2.1 Linear-non-linear adjunctions

The notion of linear-non-linear (lnl) adjunction [7] straightforwardly adapts to the setting of $\infty$ -categories. It consists in a suitable adjunction between a category ${\mathcal{L}}$ , corresponding to the “linear” formulas, and a category ${\mathcal{M}}$ which provides the “multiple” structure. The model of linear logic actually lives in the linear category: the multiplicative one is here to ensure that it is equipped with an exponential modality, namely the comonad $\mathop{!}\equiv LM$ induced by the adjunction.

Definition 1.

An $\infty$ -categorical linear-non-linear adjunction is an adjunction

\begin{matrix}\includegraphics{dagpub-standalone-combined-2025-05-21-15-10-53-% page-2.pdf2svg.svg}\end{matrix}

(1)

between a cartesian $\infty$ -category ${\mathcal{M}}$ and a symmetric monoidal closed $\infty$ -category ${\mathcal{L}}$ , together with a structure of symmetric monoidal functor on $L$ .

$\blacktriangleright$ Remark 2.

The notion of lnl adjunction is a particular case of the one of resource modality [39] which, in our setting can be defined as an adjunction as in Equation 1 between monoidal $\infty$ -categories ${\mathcal{M}}$ and ${\mathcal{L}}$ , together with a monoidal structure on the functor $L$ (not supposing that ${\mathcal{M}}$ is cartesian nor that ${\mathcal{L}}$ is closed).

It might be surprising at first that no condition is required on $M$ . In fact, since $L$ is symmetric monoidal, $M$ is automatically lax symmetric monoidal [36, Cor 7.3.2.7]. The following formalizes the fact that objects in the image of the exponential modality can be copied and erased:

Proposition 3.

In an lnl adjunction, every object $\mathop{!}A$ is equipped with a canonical structure of a commutative comonoid.

Proof.

By [36, Cor 2.4.3.10], because ${\mathcal{M}}$ is cartesian, every object is a commutative comonoid, and the symmetric monoidal functor $L$ functor transports the commutative monoid structure to ${\mathcal{L}}$ . $\hfill\blacktriangleleft$

Seely categories.

One of the most widely used notions of categorical model of linear logic is given by the notion of a Seely category. The original definition [45] was missing an axiom which was identified later on [9]. It consists in a symmetric monoidal closed category ${\mathcal{L}}$ with finite products equipped with a comonad $\mathop{!}$ , which is a symmetric monoidal functor satisfying a particular axiom. As is, this definition does not easily generalize to $\infty$ -categories, because there is no obvious way of generating the associated higher coherences. However, the alternative characterization of Seely categories as lnl adjunctions given in [38, Prop 24 and 25] does. The following definition is based on that.

Definition 4.

An lnl adjunction Equation 1 is Seely when ${\mathcal{L}}$ is cartesian (independently of being monoidal) and the comparison functor ${\mathcal{L}}_{\mathop{!}}\to{\mathcal{M}}$ from the Kleisli $\infty$ -category of the comonad $\mathop{!}\equiv LM$ on ${\mathcal{L}}$ is an equivalence of $\infty$ -categories.

It can be shown that a right adjoint functor $G:\mathcal{D}\to\mathcal{C}$ identifies ${\mathcal{D}}$ to the Kleisli $\infty$ -category ${\mathcal{C}}_{\mathop{!}}$ (where $\mathop{!}$ is the comonad induced by the adjunction) if and only if it is essentially surjective [25, Thm 7.2]. As a consequence, we have the following alternative characterization:

Proposition 5.

An lnl adjunction Equation 1 is Seely if and only if ${\mathcal{L}}$ is cartesian and $M$ is essentially surjective.

In particular, any lnl adjunction Equation 1 with ${\mathcal{L}}$ cartesian induces a Seely one by restricting ${\mathcal{M}}$ to the essential image of $M$ .

Linear categories.

Instead of considering adjunctions with Kleisli categories, one can also consider the other extreme case of adjunctions with categories of coalgebras: those correspond to linear categories [38, Prop 29 and 30]. Below, the comparison functor is defined in [36, Def 4.7.3.4].

Definition 6.

An lnl adjunction Equation 1 is linear when the comparison functor ${\mathcal{M}}\to{\mathcal{L}}^{\mathop{!}}$ to the $\infty$ -category of coalgebras is an equivalence.

2.2 Lafont categories

An important class of models is given by Lafont categories where the exponential modality is given by the cofree commutative comonoid construction (we have seen in Proposition 3 that $\mathop{!}$ always provides commutative comonoids). Given a symmetric monoidal $\infty$ -category ${\mathcal{C}}$ , we write $\operatorname{Mon}({\mathcal{C}}$ ) for the $\infty$ -category of commutative monoids in ${\mathcal{C}}$ [36, Def 2.1.3.1] and $\operatorname{Comon}({\mathcal{C}})\equiv\operatorname{Mon}({\mathcal{C}}^{% \textnormal{op}})^{\textnormal{op}}$ the $\infty$ -category of commutative comonoids in ${\mathcal{C}}$ (in this paper, all (co)monoids considered are commutative).

Definition 7.

A Lafont $\infty$ -category is a symmetric monoidal closed $\infty$ -category ${\mathcal{C}}$ such that the forgetful functor $\operatorname{Comon}({\mathcal{C}})\to{\mathcal{C}}$ is a left adjoint.

Proposition 8.

Any Lafont $\infty$ -category ${\mathcal{C}}$ induces an lnl adjunction between ${\mathcal{C}}$ and $\operatorname{Comon}({\mathcal{C}})$ .

Proof.

The $\infty$ -category $\operatorname{Comon}({\mathcal{C}})$ is cartesian, because the opposite $\infty$ -category $\operatorname{Mon}({\mathcal{C}}^{\textnormal{op}})$ is cocartesian [36, Prop 3.2.4.7]. Moreover, the forgetful functor $\operatorname{Comon}({\mathcal{C}})\to{\mathcal{C}}$ has a canonical symmetric monoidal structure [36, Ex 3.2.4.4]. $\hfill\blacktriangleleft$ In situations where the monoidal structure on ${\mathcal{C}}$ is compatible with some limits, the cofree commutative comonoid on an object $A$ can be computed explicitly using limits, see [40]. A similar construction holds in the setting of $\infty$ -categories.

Proposition 9.

Let ${\mathcal{C}}$ be a symmetric monoidal $\infty$ -category with countable limits such that, for every object $X$ , the tensor product functor $X\otimes-:{\mathcal{C}}\to{\mathcal{C}}$ preserves countable limits. Then ${\mathcal{C}}$ is Lafont, and the free commutative comonoid on an object $A$ is given by $\prod_{n\in\mathbb{N}}(A^{\otimes n})^{\Sigma_{n}}$ , where $(A^{\otimes n})^{\Sigma_{n}}$ is the object of invariants by the group action of $\Sigma_{n}$ on $A^{\otimes n}$ (i.e. the limit of the diagram $\operatorname{B}\Sigma_{n}\to{\mathcal{C}}$ classifying this group action).

Proof.

This statement is exactly dual to [36, Ex 3.1.3.14]. $\hfill\blacktriangleleft$ The monoidal categories typically appearing in linear algebra are more often compatible with colimits than with limits (that is for instance the case of categories of $R$ -modules). In such situations, we can still construct a structure of Lafont category when ${\mathcal{C}}$ is presentable, although the free commutative comonoid does not admit a nice formula as above.

Theorem 10.

Let ${\mathcal{C}}$ be a symmetric monoidal presentable $\infty$ -category such that for every object $A\in{\mathcal{C}}$ , the tensor product functor $A\otimes-:{\mathcal{C}}\to{\mathcal{C}}$ preserves small colimits. Then $\operatorname{Comon}({\mathcal{C}})$ is presentable and ${\mathcal{C}}$ is Lafont.

Proof of Theorem 10.

Since ${\mathcal{C}}$ is presentable and $A\otimes-:{\mathcal{C}}\to{\mathcal{C}}$ preserves small colimits, it admits a right adjoint, so ${\mathcal{C}}$ is monoidal closed. If we suppose that $\operatorname{Comon}({\mathcal{C}})$ is presentable, the forgetful functor $U:\operatorname{Mon}({\mathcal{C}}^{\textnormal{op}})\to{\mathcal{C}}^{% \textnormal{op}}$ preserves (and even creates) small limits by [36, Cor 3.2.2.5], so the forgetful functor $U^{\textnormal{op}}:\operatorname{Comon}({\mathcal{C}})\to{\mathcal{C}}$ preserves small colimits. By the adjoint functor theorem for presentable $\infty$ -categories [35, Cor 5.5.2.9], it must admit a right adjoint, and we have a structure of Lafont $\infty$ -category on $\mathcal{C}$ .

We are left with showing that $\operatorname{Comon}({\mathcal{C}})$ is presentable. Note that this does not immediately follow from a presentability criterion for $\infty$ -categories of monoids [36, Cor 3.2.4.5], since $\operatorname{Comon}({\mathcal{C}})$ is defined as the opposite of an $\infty$ -category of monoids, and presentability is not a self-dual notion. Nevertheless, we can adapt the proof of [36, Cor 3.2.3.5]. We say an $\infty$ -category ${\mathcal{C}}$ is copresentable if its opposite $\infty$ -category is presentable, and similarly for coaccessible. Our goal is to show that $\operatorname{Mon}({\mathcal{C}}^{\textnormal{op}})$ is copresentable, i.e. admits small limits and it is coaccessible. The $\infty$ -category $\operatorname{Mon}({\mathcal{C}}^{\textnormal{op}})$ admits small limits, once again by [36, Cor 3.2.2.5] (since ${\mathcal{C}}$ admits small colimits by virtue of being presentable, ${\mathcal{C}}^{\textnormal{op}}$ admits small limits). It can be shown to be coaccessible by [35, Thm 5.4.7.11], see Lemma 37 for details. $\hfill\blacktriangleleft$ In the case of vector spaces, the construction of free commutative comonoids (often called coalgebras in this context) dates back to Sweedler [46], and Barr [4] for modules.

2.3 $\ast$ -autonomous categories

In this section, we consider a symmetric monoidal closed $\infty$ -category $\mathcal{C}$ (with $\otimes$ as tensor and $\multimap$ as internal hom) equipped with a distinguished object $\bot$ . For an object $A\in{\mathcal{C}}$ , we write $A^{*}\equiv A\multimap\bot$ . The notion of model for classical linear logic is given by the following notion.

Definition 11 ( $\ast$ -autonomous $\infty$ -category).

The object $\bot\in{\mathcal{C}}$ is dualizing if the internal hom functor $(-)^{*}:{\mathcal{C}}^{\textnormal{op}}\to{\mathcal{C}}$ is an equivalence of $\infty$ -categories. An $\infty$ -category equipped with a dualizing object is called $\ast$ -autonomous.

Note that the dualizing object is part of the data: a given $\infty$ -category might admit multiple non-isomorphic dualizing objects, see Remark 35. We have the following alternative definition:

Proposition 12.

The object $\bot\in{\mathcal{C}}$ is dualizing if and only if for every object $A\in{\mathcal{C}}$ , the canonical map $A\to A^{**}$ is an isomorphism in ${\mathcal{C}}$ .

Proof.

Since ${\mathcal{C}}$ is symmetric monoidal, we have the following isomorphisms

\operatorname{Hom}_{\mathcal{C}}(A,B^{*})\simeq\operatorname{Hom}_{\mathcal{C}% }(A\otimes B,\bot)\simeq\operatorname{Hom}_{\mathcal{C}}(B\otimes A,\bot)% \simeq\operatorname{Hom}_{\mathcal{C}}(B,A^{*})\simeq\operatorname{Hom}_{{% \mathcal{C}}^{\textnormal{op}}}(A^{*},B)

natural in $A$ and $B$ , and the functor $(-)^{*}:{\mathcal{C}}^{\textnormal{op}}\to{\mathcal{C}}$ is thus left adjoint to $(-)^{*}:{\mathcal{C}}\to{\mathcal{C}}^{\textnormal{op}}$ . The canonical map $A\to A^{**}$ is the unit of this adjunction (as a morphism in ${\mathcal{C}}$ ) and also its counit (as a morphism in ${\mathcal{C}}^{\textnormal{op}})$ . An adjunction is an equivalence if and only if its unit and counit are isomorphisms, which gives the desired result. $\hfill\blacktriangleleft$

Proposition 13.

Suppose $({\mathcal{C}},\bot)$ is $\ast$ -autonomous. If the forgetful functor $\operatorname{Mon}({\mathcal{C}})\to{\mathcal{C}}$ admits a left adjoint $F$ (i.e. admits free commutative monoids), then ${\mathcal{C}}$ is Lafont (i.e. admits cofree commutative comonoids). Moreover, the underlying object of the free comonoid on $X\in{\mathcal{C}}$ is given by $(F(X^{*}))^{*}$ .

Proof.

Since $F:{\mathcal{C}}\to\operatorname{Mon}({\mathcal{C}})$ is a left adjoint, $F^{\textnormal{op}}:{\mathcal{C}}^{\textnormal{op}}\to\operatorname{Mon}({% \mathcal{C}})^{\textnormal{op}}$ is a right adjoint. Using the equivalence $(-)^{*}:{\mathcal{C}}\simeq{\mathcal{C}}^{\textnormal{op}}$ and passing to $\infty$ -categories of monoids, we get $\operatorname{Mon}({\mathcal{C}})^{\textnormal{op}}\simeq\operatorname{Mon}({% \mathcal{C}}^{\textnormal{op}})^{\textnormal{op}}=\operatorname{Comon}({% \mathcal{C}})$ . Hence the composite

defines a right adjoint to the forgetful functor $\operatorname{Comon}({\mathcal{C}})\to{\mathcal{C}}$ . Unfolding this composition, we also get the desired formula for the free comonoid on $X$ . $\hfill\blacktriangleleft$

We conclude this section with a small lemma that will be useful in the proof of Theorem 23. For any pair of objects $A,B\in{\mathcal{C}}$ , write $\varepsilon_{A}^{B}:B\otimes(B\multimap A)\to A$ for the evaluation map, i.e. the counit of the adjunction $B\otimes-\dashv B\multimap-$ evaluated at $A$ . Similarly, write $\eta_{A}^{B}:A\to B\multimap(B\otimes A)$ for the unit of the same adjunction.

Lemma 14.

Let $A$ be objects of ${\mathcal{C}}$ , and $f:A\xrightarrow{\sim}A^{**}$ an isomorphism. If the following square commutes

where $\sigma$ comes from the symmetry of the monoidal structure, then the canonical morphism $A\to(A\multimap\bot)\multimap\bot$ is an isomorphism.

Proof.

We have the following commuting diagram:

The left square commutes by naturality of $\eta^{A^{*}}$ . The right square commutes by assumption and functoriality of $A^{*}\multimap-$ . The composition of the bottom line is homotopic to the identity by the zig-zag identity for the adjunction $(A^{*}\otimes-)\dashv(A^{*}\multimap-)$ , in particular it is an isomorphism. Since $f$ is also an isomorphism, the composite of the top line, i.e. the canonical map $A\multimap A^{**}$ , must also be an isomorphism. $\hfill\blacktriangleleft$

3 Models of linear logic in 1-categories

In this section, we briefly recall some traditional models of linear logic, that we generalize to the $\infty$ -categorical setting later on. We first provide two models based on the powerset monad on $\operatorname{Set}$ , and then one based on vector spaces (or, more generally, modules). As we have seen in previous section, there are two canonical ways to construct lnl adjunctions. Namely, starting from a “linear” category equipped with a suitable comonad, one can either consider the category of coalgebras, or the category of free coalgebras, as the corresponding “multiple” category: this is the idea behind the notions of linear and Seely lnl adjunctions. There are actually two other canonical ways to construct lnl adjunctions. We can, dually, start from a “multiple” category equipped with a suitable monad and construct the “linear” category as the category of algebras, or free algebras, of the monad. Moreover, we can alternatively perform those constructions in order to build richer models. Let us illustrate this on three examples.

3.1 Relational polynomials

We write $\operatorname{Set}$ for the category of sets and functions, and $\operatorname{Rel}$ for the category of sets and relations: a morphism $f:A\to B$ is a relation $f\subseteq A\times B$ . This category is symmetric monoidal when equipped with the set-theoretic cartesian product on objects. It is easily checked to be self-dual compact closed, and thus closed as a monoidal category. This category is also cartesian, with product being given by set-theoretic disjoint union (this is in fact a biproduct). The canonical inclusion functor $F:\operatorname{Set}\to\operatorname{Rel}$ is symmetric monoidal, and admits a right adjoint $G:\operatorname{Rel}\to\operatorname{Set}$ which sends a set $A$ to the powerset $\mathcal{P}(A)$ and a relation $f:A\to B$ to the function which to $X\in\mathcal{P}(A)$ associates $\{y\in B\mid\exists x\in X.(x,y)\in f\}$ . The monad induced on $\operatorname{Set}$ is the powerset monad, whose Kleisli category is precisely $\operatorname{Rel}$ . Namely, the isomorphism is given on hom-sets by $(A\to\mathcal{P}(B))\simeq(A\to(B\to 2))\simeq(A\times B\to 2)$ where $2$ is the set with two elements. We have thus constructed an lnl adjunction between $\operatorname{Set}$ and $\operatorname{Rel}$ .

Consider the free commutative monoid monad $M$ on $\operatorname{Set}$ . There is a distributive law $\lambda:M\circ\mathcal{P}\to\mathcal{P}\circ M$ between the two monads (given a set $A$ , $\lambda_{A}$ sends a formal product of subsets $X_{1}\ldots X_{n}$ to the subset of formal products $\{x_{1}\ldots x_{n}\mid x_{i}\in X_{i}\}$ ), and the monad $M$ thus lifts to the Kleisli category $\operatorname{Rel}$ [6]. Since $\operatorname{Rel}$ is self-dual this monad, that we denote $\mathop{!}$ , is also a comonad. We write $\operatorname{Poly}$ for the co-Kleisli category: a morphism $P:A\to B$ is a relation $P:\mathop{!}A\to B$ , which can be thought of as encoding a family of polynomials

\Big{(}\sum_{((a_{1},\ldots,a_{n}),b)\in P}X_{a_{1}}\ldots X_{a_{n}}\Big{)}_{b% \in B}

which take variables typed in $A$ and returns polynomials typed in $B$ , and composition corresponds to the expected one for polynomials. Note that each polynomial contains at most once a monomial, i.e. we have “boolean coefficients”, but might consist of an infinite sum. This category is cartesian, with cartesian product given by set-theoretic disjoint union on objects. The resulting adjunction between $\operatorname{Poly}$ and $\operatorname{Rel}$ forms a Seely category lnl adjunction. It turns out that $\operatorname{Rel}$ is also a Lafont category, and the comonad just described is isomorphic to the one given by the free commutative comonoid in $\operatorname{Rel}$ . Higher-categorical variants of this model have been considered in the literature such as generalized species of structures [16], operads [10] or polynomial functors [33, 23].

3.2 Domains

As a variant of the previous construction, we can start from the category algebras of the powerset monad on $\operatorname{Set}$ (instead of the associated Kleisli category). This is equivalent to the category $\operatorname{CSL}$ of complete (sup) semilattices and sup-preserving functions. Indeed, an algebra $f:\mathop{!}A\to A$ induces a partial order on $A$ given by $x\leq y$ whenever $f(\{x,y\})=y$ , and, given $X\subseteq A$ , its least upper bound is given by $f(X)$ . As for any category of algebras, there is an adjunction where the right adjoint $\operatorname{CSL}\to\operatorname{Set}$ sends a complete semilattice to the underlying set, and the left adjoint $\operatorname{Set}\to\operatorname{CSL}$ sends a set to the power set semilattice, ordered by inclusion. The category $\operatorname{CSL}$ is cartesian with the usual cartesian product of posets (or categories). It is also monoidal for the tensor $A\otimes B$ representing functions from $A\times B$ which preserve sups in each coordinate [17]: it can be constructed as the set of downward closed subsets $I$ of $A\times B$ such that for $X\subseteq A$ and $Y\subseteq B$ such that $X\times Y\subseteq I$ we have $(\bigvee X,\bigvee Y)\in I$ . This tensor product has an internal hom (given by $\operatorname{Hom}_{\operatorname{CSL}}$ equipped with the pointwise ordering), giving rise to a $*$ -autonomous category which is not compact closed [5].

The category $\operatorname{Dom}$ of domains is the category of directed-complete (sup) semi-lattices and Scott continuous functions (preserving the sups of directed sets). This category is cartesian closed, and the forgetful functor $\operatorname{CSL}\to\operatorname{Dom}$ admits a symmetric monoidal left adjoint, thus giving an lnl adjunction. This construction is hinted at in [1, Section 8.3.3].

3.3 Modules

We finally present a model based on vector spaces, which is arguably one of the reasons why linear logic is called so. For the sake of generality, we actually consider modules over a ring. Given a commutative ring $R$ , we recall that an $R$ -module is an abelian group $(M,+,0)$ together with a scalar multiplication operation $-\cdot-:R\times M\to M$ satisfying $a\cdot(m+m^{\prime})=am+am^{\prime}$ , $(a+b)\cdot m=am+bm$ and $(ab)\cdot m=a\cdot(b\cdot m)$ . A morphism of $R$ -modules is a morphism of the underlying abelian groups $f:M\to M^{\prime}$ which is compatible with the scalar multiplication. We write $\operatorname{Mod}_{R}$ for the category of $R$ -modules and $R$ -module morphisms. In particular, when $R\equiv\mathbb{Z}$ , $\operatorname{Mod}_{\mathbb{Z}}$ is the category $\operatorname{Ab}$ of abelian groups, and, when $R\equiv k$ is a field, $\operatorname{Mod}_{k}$ is the category $\operatorname{Vect}_{k}$ of $k$ -vector spaces.

The category $\operatorname{Mod}_{R}$ admits a symmetric monoidal structure given by the tensor product of $R$ -modules: the $R$ -module $A\otimes B$ represent bilinear functions from $A\times B$ . The ring $R$ , seen as an $R$ -module with multiplication as scalar multiplication, is a neutral element. The forgetful functor $U:\operatorname{Mod}_{R}\to\operatorname{Set}$ has a left adjoint $R[-]:\operatorname{Set}\to\operatorname{Mod}_{R}$ , sending a set $X$ to the free $R$ -module $R[X]\equiv\bigoplus_{x\in X}R$ , which is symmetric monoidal (with $\operatorname{Set}$ equipped with its cartesian monoidal structure), thus giving rise to the lnl adjunction on the left, which specializes to the two other lnl adjunctions when $R\equiv\mathbb{Z}$ and $R\equiv k$ :

Note that $\operatorname{Mod}_{R}$ is also a Lafont category (see [27, Section 2.4], [4], or [46, Thm 6.4.3] for the case of vector spaces), which can be recovered as a consequence of Theorem 10, but the Lafont comonad is different from the one just described and in general hard to describe. This is however not a $\ast$ -autonomous category (and thus not a model of classical linear logic): since it is presentable, $\ast$ -autonomy would imply that its opposite is also presentable, and thus that it is a poset [2, Thm 1.64]. This limitation can be overcome by restricting to finite-dimensional vector spaces over fields which are finite [48] or in characteristic 2 [27, Sec 2.4] (in order to keep the exponential finite) or considering topological vector spaces [31].

4 Models in $\infty$ -categories with colimits

$\infty$ -categorical domains.

In this section, we construct an $\infty$ -categorical model by generalizing the model of domains recalled in Section 3.2. Basically, we replace (sup-complete) posets by (cocomplete) $\infty$ -categories, continuous functions by colimit-preserving functors, and Scott-continuous by filtered-colimit-preserving functors.

Given a class ${\mathcal{K}}$ of (small) simplicial sets, we write $\operatorname{Cat}({\mathcal{K}})$ for the $\infty$ -category of (possibly large) $\infty$ -categories that admit ${\mathcal{K}}$ -colimits and functors that preserve such colimits. In the case where ${\mathcal{K}}$ is the collection of filtered $\infty$ -categories, we write $\operatorname{Cat_{filtr}}\equiv\operatorname{Cat}({\mathcal{K}})$ . When ${\mathcal{K}}$ is the class of all (small) simplicial sets, we write $\operatorname{Cat_{cc}}\equiv\operatorname{Cat}({\mathcal{K}})$ for the $\infty$ -category of cocomplete $\infty$ -categories.

Proposition 15.

Given any two classes of simplicial sets ${\mathcal{K}}\subseteq{\mathcal{K}}^{\prime}$ we have an adjunction $\begin{matrix}\includegraphics{dagpub-standalone-combined-2025-05-21-15-10-53-% page-12.pdf2svg.svg}\end{matrix}$ between symmetric monoidal $\infty$ -categories where $U:\operatorname{Cat}({\mathcal{K}})\to\operatorname{Cat}({\mathcal{K}}^{\prime})$ is the forgetful functor and the left adjoint ${\mathcal{P}}_{\mathcal{K}}^{{\mathcal{K}}^{\prime}}:\operatorname{Cat}({% \mathcal{K}}^{\prime})\to\operatorname{Cat}({\mathcal{K}})$ is symmetric monoidal.

Proof.

By [35, Cor 5.3.6.10], the forgetful functor $U$ admits a left adjoint. By [36, Cor 4.8.1.4], the $\infty$ -category $\operatorname{Cat}({\mathcal{K}})$ (and similarly for $\operatorname{Cat}({\mathcal{K}}^{\prime})$ ) admits a symmetric monoidal structure, where the tensor ${\mathcal{C}}\otimes{\mathcal{D}}$ represent functors from ${\mathcal{C}}\times{\mathcal{D}}$ which preserve ${\mathcal{K}}$ -colimits in each variable, and this monoidal structure is closed [36, Rem 4.8.1.6]. Finally, the left adjoint ${\mathcal{P}}_{\mathcal{K}}^{{\mathcal{K}}^{\prime}}$ admits a structure of symmetric monoidal functor [36, Rem 4.8.1.8]. $\hfill\blacktriangleleft$

Theorem 16.

There is a linear non-linear adjunction $\begin{matrix}\includegraphics{dagpub-standalone-combined-2025-05-21-15-10-53-% page-13.pdf2svg.svg}\end{matrix}$

Proof.

By Proposition 15, we only need to show that the monoidal structure on $\operatorname{Cat_{filtr}}$ is cartesian. Every filtered $\infty$ -category is sifted [35, Ex 5.5.8.3], and we conclude with [36, Rem 4.8.1.5]. More explicitly, this comes from the fact that a functor ${\mathcal{C}}\times{\mathcal{C}}^{\prime}\to{\mathcal{D}}$ preserves sifted colimits if and only if it preserves sifted colimits in both variables [35, Prop 5.5.8.6]. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 17.

With the model of Sections 3.2 and 15 in mind, we could have considered different generalizations of the notion of directed families. For instance, we could have taken sifted $\infty$ -categories instead of filtered ones and obtained another lnl adjunction. Finally, one could also replace $\operatorname{Cat_{filtr}}$ by $\operatorname{Cat}$ and obtain yet another lnl adjunction, and even $\operatorname{Cat}$ by ${\mathcal{S}}$ by taking the underlying core of an $\infty$ -category. To sum all of this up, there really is a chain of symmetric monoidal left adjoints

where the monoidal structures on ${\mathcal{S}}$ , $\operatorname{Cat}$ , $\operatorname{Cat_{filtr}}$ and $\operatorname{Cat}_{\textnormal{sift}}$ are all cartesian.

$\infty$ -categorical relations.

We now investigate an $\infty$ -categorical version of the model of relations presented in Section 3.1. The natural generalization of the powerset monad on $\operatorname{Set}$ is the free cocompletion monad $\mathcal{P}$ on $\operatorname{Cat}$ , which exists by general arguments (we can take $\mathcal{P}\equiv{\mathcal{P}}_{\emptyset}^{\operatorname{sSet}}$ as defined in Proposition 15). When $\mathcal{C}$ is a small $\infty$ -category, $\mathcal{P}(\mathcal{C})$ coincides with the presheaf $\infty$ -category $\widehat{\mathcal{C}}\equiv\operatorname{Fun}(\mathcal{C}^{\textnormal{op}},% \mathcal{S})$ . We have seen in previous section that $\operatorname{Cat_{cc}}$ plays a analogous role to the $\operatorname{CSL}$ category (the category of algebras of the powerset monad), and we should thus recover a $\infty$ -categorical counterpart to $\operatorname{Rel}$ by restricting to “free algebras”, i.e. objects of the form $\mathcal{P}(X)$ for $X\in\mathcal{S}$ . It turns out to be convenient to consider the following variant of this construction:

Definition 18.

We write $\operatorname{Cat_{prof}}$ for the full subcategory of $\operatorname{Cat_{cc}}$ spanned by $\infty$ -categories of the form $\widehat{{\mathcal{C}}}$ for some small $\infty$ -category ${\mathcal{C}}$ .

$\blacktriangleright$ Remark 19.

The notation $\operatorname{Cat_{prof}}$ is due to the fact that $[\widehat{\mathcal{C}},\widehat{\mathcal{D}}]_{\textnormal{cc}}\simeq[{% \mathcal{C}},\widehat{\mathcal{D}}]$ , the $\infty$ -category of profunctors from ${\mathcal{C}}\to{\mathcal{D}}$ . Hence one might be tempted to see $\operatorname{Cat_{prof}}$ as an $\infty$ -category whose objects are small $\infty$ -categories and morphisms are profunctors. This intuition is almost right, up to a slight subtlety: two non-equivalent small $\infty$ -categories ${\mathcal{C}}$ and ${\mathcal{D}}$ may yield the same presheaf $\infty$ -category $\widehat{\mathcal{C}}\simeq\widehat{\mathcal{D}}$ . It turns out that this happens precisely if ${\mathcal{C}}$ and ${\mathcal{D}}$ have the same idempotent completion [37, Tag 040X], so we can think of $\operatorname{Cat_{prof}}$ as the $\infty$ -category of small idempotent complete $\infty$ -categories and profunctors between them.

Proposition 20.

The symmetric monoidal structure on $\operatorname{Cat_{cc}}$ restricts to $\operatorname{Cat_{prof}}$ . Moreover, we have $\widehat{1}\simeq{\mathcal{S}}$ and $\widehat{\mathcal{C}}\otimes\widehat{\mathcal{D}}\simeq\widehat{{\mathcal{C}}% \times{\mathcal{D}}}$ .

Proof.

The free cocompletion functor $\widehat{(-)}:\operatorname{Cat}\to\operatorname{Cat_{cc}}$ is symmetric monoidal, and the monoidal structure on $\operatorname{Cat}$ is cartesian by [36, Rem 4.8.1.5], in particular we get isomorphisms ${\mathcal{S}}\simeq\widehat{1}$ and $\widehat{\mathcal{C}}\otimes\widehat{\mathcal{D}}\simeq\widehat{{\mathcal{C}}% \times{\mathcal{D}}}$ . It remains to show that the monoidal structure on $\operatorname{Cat}$ preserves smallness: the terminal $\infty$ -category is clearly small and the cartesian product of small $\infty$ -categories is still a small $\infty$ -category. $\hfill\blacktriangleleft$

Theorem 21.

The $\infty$ -category $\operatorname{Cat_{cc}}$ admits small colimits, and the monoidal structure is compatible with small colimits.

Proof.

The proof can be done as the one of [36, Prop 4.8.4.2], but without the smallness assumption on the class of simplicial sets ${\mathcal{K}}$ . See Section A.2 for details. $\hfill\blacktriangleleft$

Lemma 22.

The forgetful functor $\operatorname{Mon}(\operatorname{Cat_{cc}})\to\operatorname{Cat_{cc}}$ has a left adjoint $\operatorname{Sym}_{\textnormal{cc}}$ . The free monoid on a presheaf $\infty$ -category $\widehat{{\mathcal{C}}}$ is given by $\widehat{\operatorname{Sym}({\mathcal{C}})}$ where $\operatorname{Sym}$ denotes the free symmetric monoidal $\infty$ -category construction (i.e. the left adjoint to $\operatorname{Mon}(\operatorname{Cat})\to\operatorname{Cat}$ ).

Proof.

That the forgetful functor $\operatorname{Mon}(\operatorname{Cat_{cc}})\to\operatorname{Cat_{cc}}$ admits a left adjoint follows from [36, Ex 3.1.3.14] and Theorem 21. Again invoking [36, Ex 3.1.3.14], the $\infty$ -category $\operatorname{Cat}$ with its cartesian symmetric monoidal structure admits free monoids. In other words, we can form free symmetric monoidal $\infty$ -categories (and they can be computed using the usual formula $\coprod_{n}{\mathcal{C}}^{n}\mathbin{\!\!/\!\!/\!}\Sigma_{n}$ , the disjoint union of the homotopy quotients of $\mathcal{C}^{n}$ under the action of the symmetric group of degree $n$ ). Moreover, the left adjoint $\mathcal{P}$ to the forgetful functor $U:\operatorname{Cat_{cc}}\to\operatorname{Cat}$ being symmetric monoidal, its right adjoint is lax symmetric monoidal [36, Cor 7.3.2.7], so they induce an adjunction

and the commutativity of the following square of forgetful right adjoint functors shown below on the right implies the commutativity of the square of their left adjoints (on the left below).

This means that the functor $\mathcal{P}$ preserves the “freeness” of monoids. If ${\mathcal{C}}$ is a small $\infty$ -category, so is $\operatorname{Sym}({\mathcal{C}})$ , and $\mathcal{P}(\operatorname{Sym}({\mathcal{C}}))=\widehat{\operatorname{Sym}({% \mathcal{C}})}$ , which gives the desired result. $\hfill\blacktriangleleft$

Theorem 23.

$\operatorname{Cat_{prof}}$ is a Lafont $\infty$ -category. The free commutative comonoid on $\widehat{\mathcal{C}}$ is $\widehat{\operatorname{Sym}{\mathcal{C}}}$ .

$\blacktriangleright$ Remark 24.

The authors of [16] have described a cartesian closed bicategory in which objects are small categories and morphisms are profunctors $\operatorname{Sym}{\mathcal{C}}\relbar\joinrel\mapstochar\joinrel\rightarrow{% \mathcal{D}}$ (called generalized species). In [15], they extend upon this result by explicitly building a “bicategorical model” of differential linear logic, based on the comonad $\operatorname{Sym}$ on the bicategory of small categories and profunctors. As discussed at the beginning of this section, $\operatorname{Cat_{prof}}$ can thought of as the $\infty$ -category of small $\infty$ -categories and $\infty$ -profunctors. The formula given by the theorem for the free commutative monoid on $\widehat{{\mathcal{C}}}$ shows that this model is an $\infty$ -categorical generalization of the one of [15]. Note however that their model is bicategorical in a full $(2,2)$ -categorical sense, while ours is $(\infty,1)$ -categorical. We expect our model to be generalizable to the $(\infty,2)$ -categorical setting and the results of [15] to hold there.

$\blacktriangleright$ Remark 25.

Restricting $\operatorname{Cat_{prof}}$ to $\infty$ -categories of the form $\widehat{X}$ where $X$ is an $\infty$ -groupoid still yields a Lafont $\infty$ -category (in view of the formula for the comonad). Then, we have $\operatorname{Cat_{prof}}(\widehat{X},\widehat{Y})\simeq\operatorname{Fun}(X% \times Y,{\mathcal{S}})\simeq{\mathcal{S}}_{/X\times Y}\simeq\operatorname{% Span}(X,Y)$ , the $\infty$ -category of spans between $X$ and $Y$ . In view of this, this model restricted to $\infty$ -groupoids can be seen as a fully homotopy coherent version of the “wild” model of spans and polynomial functors described by the authors in [23].

Proof of Theorem 23.

In view of the formula for the left adjoint to the forgetful functor $\operatorname{Mon}(\operatorname{Cat_{cc}})\to\operatorname{Cat_{cc}}$ given for presheaf $\infty$ -categories in Lemma 22, we see that the free/forgetful adjunction restricts to one between $\operatorname{Cat_{prof}}$ and $\operatorname{Mon}(\operatorname{Cat_{prof}})$ . To obtain a Lafont model, we are going to use Proposition 13 and we are left with showing that $\operatorname{Cat_{prof}}$ is $\ast$ -autonomous. Having done that, the formula for the free commutative comonoid will also follow from Proposition 13 and the observation that $(\operatorname{Sym}{\mathcal{C}}^{\textnormal{op}})^{\textnormal{op}}\simeq% \operatorname{Sym}{\mathcal{C}}$ .

We now show that ${\mathcal{S}}=\widehat{1}$ is a dualizing object in $\operatorname{Cat_{prof}}$ . For every small $\infty$ -category ${\mathcal{C}}$ , we write $\text{\char 72\relax}_{\mathcal{C}}:{\mathcal{C}}\to\widehat{{\mathcal{C}}}$ for the yoneda embedding. We write $[-,-]_{\textnormal{cc}}$ for the internal hom in $\operatorname{Cat_{cc}}$ . Given a cocomplete $\infty$ -category ${\mathcal{D}}$ , the restriction functor $-\circ\text{\char 72\relax}_{\mathcal{C}}:[\widehat{{\mathcal{C}}},{\mathcal{D% }}]_{\textnormal{cc}}\to[{\mathcal{C}},{\mathcal{D}}]$ is an equivalence, with inverse $\operatorname{Lan}_{\text{\char 72\relax}_{\mathcal{C}}}:[{\mathcal{C}},{% \mathcal{D}}]\to[\widehat{{\mathcal{C}}},{\mathcal{D}}]_{\textnormal{cc}}$ given by left Kan extension along $\text{\char 72\relax}_{\mathcal{C}}$ [35, Thm 5.1.5.6].

Let ${\mathcal{C}}$ be a small $\infty$ -category. Write $f$ for the composite of the following sequence of equivalences of $\infty$ -categories

To show that the canonical morphism $\widehat{{\mathcal{C}}}\to[[\widehat{{\mathcal{C}}},{\mathcal{S}}]_{% \textnormal{cc}},{\mathcal{S}}]_{\textnormal{cc}}$ is an equivalence, it suffices to show that $f$ satisfies the commutativity condition of Lemma 14. Since the tensor product of $\infty$ -categories with colimits classifies functors that preserve colimits in both variables, this reduces to showing that the following diagram of $\infty$ -categories commute.

Simplifying furthermore through the equivalence $\operatorname{Lan}_{\text{\char 72\relax}_{\mathcal{C}}}:\widehat{{\mathcal{C}% }^{\textnormal{op}}}\to[\widehat{{\mathcal{C}}},{\mathcal{S}}]_{\textnormal{cc}}$ , this amounts to showing that the two following maps $\widehat{{\mathcal{C}}^{\textnormal{op}}}\times\widehat{{\mathcal{C}}}\to{% \mathcal{S}}$ are naturally isomorphic:

\displaystyle(F,G)

\displaystyle\mapsto\operatorname{Lan}_{\text{\char 72\relax}_{\mathcal{C}}}(F% )(G)

\displaystyle(F,G)

\displaystyle\mapsto\operatorname{Lan}_{\text{\char 72\relax}_{{\mathcal{C}}^{% \textnormal{op}}}}(G)(F)

According to [24, Prop 4.8], those left Kan extensions can be computed as weighted colimits, which themselves can be defined as coends, so that the desired isomorphism becomes

\int^{c\in{\mathcal{C}}}F(c)\times G(c)\simeq\int^{c\in{\mathcal{C}}^{% \textnormal{op}}}G(c)\times F(c)

This isomorphism itself follows from the symmetry of the cartesian product together with the self-duality of coends, which can be seen easily through the definition of coends as colimits indexed on the twisted arrow $\infty$ -category $\textnormal{Tw}({\mathcal{C}})$ [24, Cor 3.8] together with the equivalence $\textnormal{Tw}({\mathcal{C}})\simeq\textnormal{Tw}({\mathcal{C}}^{\textnormal% {op}})$ [37, Tag 03JL]. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 26.

The reader may recognize the formula $\int^{c\in{\mathcal{C}}}F(c)\times G(c)$ as the definition of the tensor product of the copresheaf $F$ with the presheaf $G$ . This tensor product is characterized as being cocontinuous in both its arguments and being the $\operatorname{Hom}$ functor ${\mathcal{C}}^{\textnormal{op}}\times{\mathcal{C}}\to{\mathcal{S}}$ when restricted to representable (co)presheaves. In a sense, we just proved that the evaluation functors $\widehat{{\mathcal{C}}}^{\ast}\times\widehat{{\mathcal{C}}}^{(**)}\to{\mathcal% {S}}$ simply reduce to extensions of the $\operatorname{Hom}$ functor, which can be thought of as a generalization of the Yoneda lemma.

5 Spectra

Having generalized models of linear logic based on domains and relations in Section 4, we now turn to $\infty$ -categorical versions of linear algebraic models. Using the cartesian symmetric monoidal structure on ${\mathcal{S}}$ , one can consider the $\infty$ -category $\operatorname{Mon}({\mathcal{S}})$ (or simply $\operatorname{Mon}$ ) of commutative monoids in ${\mathcal{S}}$ . A commutative monoid $M\in\operatorname{Mon}$ is said to be a commutative group if for every $x\in M$ , the multiplication map $x\cdot-:M\to M$ is an isomorphism of $\infty$ -groupoids. The full subcategory of $\operatorname{Mon}$ spanned by the commutative groups is written $\operatorname{Grp}({\mathcal{S}})$ (or simply $\operatorname{Grp}$ ). To generalize the lnl adjunction between $\operatorname{Set}$ and $\operatorname{Ab}$ to the $\infty$ -categorical setting, we could look for an lnl adjunction between ${\mathcal{S}}$ and $\operatorname{Grp}$ . The first step would thus be to find a symmetric monoidal structure on $\operatorname{Grp}$ . We could do this directly, but we prefer to take a small detour to explore a bigger $\infty$ -category of interest in homotopy theory: the $\infty$ -category of spectra [36, Def 1.4.3.1].

We write ${\mathcal{S}}_{*}$ for the $\infty$ -category of pointed $\infty$ -groupoids, i.e. $\infty$ -groupoids $X$ equipped with a distinguished object $\star_{X}$ . Given $X\in{\mathcal{S}}_{*}$ , we write $\operatorname{\Omega}X=\operatorname{Hom}_{X}(\star_{X},\star_{X})$ for its loop space, and $\pi_{n}(X)\equiv\pi_{0}(\operatorname{\Omega}^{n}X)$ where $\pi_{0}(X)$ is the set of connected components of $X$ .

Definition 27.

A spectrum is a sequence of pointed $\infty$ -groupoids $(X_{n})_{n\in\mathbb{N}}$ together with pointed isomorphisms $X_{n}\simeq\operatorname{\Omega}X_{n+1}$ for every $n\in\mathbb{N}$ . The $\infty$ -category $\operatorname{Sp}$ of spectra is by definition the limit of the infinite tower of $\infty$ -categories . The forgetful functor $\operatorname{Sp}\to{\mathcal{S}}_{*}$ , $(X_{n})\mapsto X_{0}$ is called the infinite loopspace functor and is written $\operatorname{\Omega}^{\infty}$ .

Let $(X_{n})$ be a spectrum. We have $\pi_{0}(X_{0})\simeq\pi_{1}(X_{1})$ , so $\pi_{0}(X_{0})$ comes equipped with a group structure. But we also have $\pi_{0}(X_{0})\simeq\pi_{2}(X_{2})$ , so this group structure is abelian. In a sense, the infinite sequence of deloopings of $X_{0}$ equip it with a commutative group structure, and indeed if all the $X_{i}$ are connected, then their data is precisely equivalent to the data of a commutative group structure on $X_{0}$ .

Definition 28.

A spectrum in which $X_{n}$ is connected when $n\geq 1$ is said to be connective. The full subcategory of $\operatorname{Sp}$ spanned by the connective spectra is written $\operatorname{Sp}^{\textnormal{cn}}$ .

Spectra can be thought of as a generalization of the notion of commutative group, in the sense that we have an equivalence of $\infty$ -categories $\operatorname{Grp}\simeq\operatorname{Sp}^{\textnormal{cn}}$ [36, Rmk 5.2.6.26]. The infinite loopspace functor $\operatorname{\Omega}^{\infty}$ has a left adjoint $\operatorname{\Sigma}^{\infty}:{\mathcal{S}}_{*}\to\operatorname{Sp}$ [36, proof of Prop 1.4.3.4], whose essential image is contained in $\operatorname{Sp}^{\textnormal{cn}}$ . Under the previous equivalence, $\operatorname{\Sigma}^{\infty}$ should be thought of as computing the “free homotopy commutative group” on a pointed space $X\in{\mathcal{S}}_{*}$ .

The $\infty$ -category of pointed $\infty$ -groupoids is monoidal [36, Rmk 4.8.2.14]:

Theorem 29.

There is a symmetric monoidal structure on ${\mathcal{S}}_{*}$ , entirely characterized by its unit being the $0$ -sphere $S^{0}$ (i.e. the discrete $2$ -point space with a distinguished point) and by its tensor product preserving small colimits in both variables. This tensor product is the smash product of pointed spaces.

There is also a monoidal structure on spectra [36, Cor 4.8.2.19, Lem 7.1.1.7]:

Theorem 30.

There is a symmetric monoidal structure on $\operatorname{Sp}$ : its unit is the object $\mathbb{S}\equiv\operatorname{\Sigma}^{\infty}S^{0}$ (the sphere spectrum) and its tensor product preserves small colimits in both variables. Moreover $\mathbb{S}$ is connective and the tensor product preserves connective spectra, so this structure restricts to a symmetric monoidal structure on $\operatorname{Sp}^{\textnormal{cn}}$ .

Theorem 31.

There is a chain of symmetric monoidal left adjoints

where the symmetric monoidal structure on ${\mathcal{S}}$ is the cartesian one, the one on ${\mathcal{S}}_{*}$ is given by the smash product of Theorem 29, and the ones on $\operatorname{Sp}^{\textnormal{cn}}$ and $\operatorname{Sp}$ are the ones in Theorem 30. In particular, there is an lnl adjunction between spaces and spectra.

Proof.

Using the machinery of [36, Section 4.8.2], writing $\Pr^{L}$ for the symmetric monoidal $\infty$ -category of presentable $\infty$ -categories and cocontinuous functors (inheriting the monoidal structure from the one of Proposition 15) [36, Prop 4.8.1.15], we have that $({\mathcal{S}},1)$ , $({\mathcal{S}}_{*},S^{0})$ and $(\operatorname{Sp},\mathbb{S})$ are idempotent objects of $\Pr^{L}$ [36, Prop 4.8.2.11, Prop 4.8.2.18]. The concontinuous functors $(-)_{+}$ and $\operatorname{\Sigma}^{\infty}$ respectively map $1\in{\mathcal{S}}$ to $S^{0}\in{\mathcal{S}}_{*}$ , and $S^{0}\in{\mathcal{S}}_{*}$ to $\mathbb{S}\in\operatorname{Sp}$ , therefore, by [36, Prop 4.8.2.9], they lift to symmetric monoidal functors between the induced monoidal structures. The inclusion $\operatorname{Sp}^{\textnormal{cn}}\to\operatorname{Sp}$ is symmetric monoidal by Theorem 30. The fact that this inclusion has a right adjoint can be seen in multiple ways, for instance we can invoke the adjoint functor theorem using the fact that the inclusion preserves colimits, and showing that $\operatorname{Sp}^{\textnormal{cn}}$ is presentable by identifying $\operatorname{Grp}$ as a strongly reflective subcategory of $\operatorname{Mon}$ and using the equivalence $\operatorname{Grp}\simeq\operatorname{Sp}^{\textnormal{cn}}$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 32.

With more effort, this chain of adjunctions could be made to include the factorization ${\mathcal{S}}_{*}\to\operatorname{Mon}\to\operatorname{Grp}$ . The $\infty$ -category $\operatorname{Mon}$ is the $\infty$ -category of the ${\mathcal{S}}$ -models of the Lawvere theory of commutative monoids [8], so one can show that for any presentable $\infty$ -category ${\mathcal{C}}$ , ${\operatorname{Mon}}\otimes{\mathcal{C}}\simeq\operatorname{Mon}({\mathcal{C}})$ . In particular, $\operatorname{Mon}\otimes\operatorname{Mon}\simeq\operatorname{Mon}(% \operatorname{Mon})$ , which can be shown to be equivalent to $\operatorname{Mon}$ . This means that $\operatorname{Mon}$ is also an idempotent object of $\Pr^{L}$ , which is enough to conclude. We could also do the same reasoning with $\operatorname{Grp}$ to show that it is idempotent independently from it being a subcategory of $\operatorname{Sp}$ . We conjecture this kind of argument to be a generalization to the $\infty$ -categorical setting of a standard reasoning giving closed symmetric monoidal structures on categories of models of commutative algebraic theories [42, 30].

$\blacktriangleright$ Remark 33.

Following the preceding remark, if $X$ is a pointed connected space, i.e. satisfying $\pi_{0}(X)=1$ , then the free commutative monoid on $X$ is already a group by the James construction [12]! This fact can be used to give a formula for the comonad $\operatorname{\Sigma}^{\infty}\operatorname{\Omega}^{\infty}\mathbb{X}$ when $\mathbb{X}$ is a connected supension spectrum (i.e. lying in the image of $\operatorname{\Sigma}^{\infty}$ ): under that assumption, we have $\operatorname{\Sigma}^{\infty}\operatorname{\Omega}^{\infty}\mathbb{X}\simeq% \bigoplus_{n\geq 1}\mathbb{X}^{\otimes n}_{\Sigma_{n}}$ [3, Ex 1.2.6], which looks like the formula for the free commutative algebra (with specified unit) on $\mathbb{X}$ (note that the free commutative algebra is in general a monad, not a comonad). For that reason, the comonad $\operatorname{\Sigma}^{\infty}\operatorname{\Omega}^{\infty}$ has been conjectured to be an exponential comonad for a homotopical model of linear logic in the context of Goodwillie’s calculus of functors [43]. However, the monoidal structure on ${\mathcal{S}}_{*}$ is not cartesian, so its adjunction with $\operatorname{Sp}$ is not lnl. Instead, taking the comonad $\operatorname{\Sigma}^{\infty}\operatorname{\Omega}^{\infty}(-)_{+}$ induced by the adjunction between ${\mathcal{S}}$ and $\operatorname{Sp}$ gives the formula

\operatorname{\Sigma}^{\infty}\operatorname{\Omega}^{\infty}\mathbb{X}_{+}% \simeq\operatorname{\Sigma}^{\infty}\operatorname{\Omega}^{\infty}\mathbb{X}% \oplus\mathbb{S}\simeq\bigoplus_{n\geq 0}\mathbb{X}^{\otimes n}_{\Sigma_{n}}

for $\mathbb{X}$ a connected suspension spectrum. The added term $n=0$ makes the right handside equivalent to the free commutative algebra on $\mathbb{X}$ .

This phenomenon is truly exclusive to the homotopical setting: if one wanted to obtain a similar result for abelian groups for instance, the result is still true but the assumption of $\mathbb{X}$ being connected is only satisfied by the trivial group. In general there is no reason to expect the “free commutative group on a commutative group” comonad and the “free commutative algebra” monad to coincide.

$\blacktriangleright$ Remark 34.

Note that the symmetric monoidal $\infty$ -category $\operatorname{Sp}$ satisfies the hypotheses of Theorem 10, so in particular it is Lafont. However, similarly to the $1$ -categorical case of $R$ -modules (or vector spaces), the comonad induced by the cofree commutative comonoid and the one induced by the adjunction with ${\mathcal{S}}$ are wildly different.

$\blacktriangleright$ Remark 35.

The $\infty$ -category $\operatorname{Sp}$ is not $\ast$ -autonomous, as it is presentable (see the discussion at the end of Section 3.3). However, it is known in stable homotopy theory that every finite spectrum is dualizable (with a finite dual), so the $\infty$ -category of finite spectra is compact closed. We do not elaborate further on finite spectra or compact closedness here, but note that this should imply $\ast$ -autonomy with the unit spectrum $\mathbb{S}$ as a dualizing object. Moreover using the equivalence $\Sigma:\operatorname{Sp}_{\textnormal{Fin}}\rightleftarrows\operatorname{Sp}_{% \textnormal{Fin}}:\Omega$ , this also implies that every $\Sigma^{n}\mathbb{S}$ , with $n\in\mathbb{Z}$ , is a dualizing object. This gives an example of a $\ast$ -autonomous $\infty$ -category with multiple dualizing objects.

$\blacktriangleright$ Remark 36.

Beyond the lnl adjunctions we described in this paper, the chains of adjunctions of Remark 17, Theorem 31 and Remark 32 all give examples of resource modalities [39]. In particular, the chain of adjunctions

decomposes the linear exponential comonad $\operatorname{\Sigma}^{\infty}\operatorname{\Omega}^{\infty}(-)_{+}$ into an affine exponential $(-)_{+}$ on ${\mathcal{S}}_{*}$ followed by a relevant exponential $\operatorname{\Sigma}^{\infty}\operatorname{\Omega}^{\infty}$ on $\operatorname{Sp}$ . From the point of view of linear logic, this corresponds to considering separately the dynamics of weakening and contraction, see also [28].

6 Future work

In the proof of Theorem 23, we have shown that the symmetric monoidal $\infty$ -category $\operatorname{Cat_{prof}}$ is $\ast$ -autonomous. We actually expect it to be compact closed, i.e. that all objects admit duals in the sense of [36, Sec 4.6]. We should also prove that compact closedness implies $\ast$ -autonomy as in the $1$ -categorical case, but we do not expect any surprises there.

As said in Remark 24, we expect that the $(\infty,1)$ -category $\operatorname{Cat_{prof}}$ can be enhanced to an $(\infty,2)$ -category (for instance using its monoidal closure together with the lax monoidal forgetful functor $\operatorname{Cat_{cc}}\to\operatorname{Cat}$ ), and that it should form an $(\infty,2)$ -categorical model of differential linear logic, in a sense appropriately generalized from [15].

It has also been conjectured that Goodwillie’s calculus of functors [22, 36] should be an $(\infty,2)$ -categorical model of differential linear logic in some sense, and we hope that the theory we developed in this paper can be a first step towards the solving of that conjecture.

References

[1] Samson Abramsky and Achim Jung. Handbook of Logic in Computer Science, volume 3, chapter Domain theory, pages 1–168. Clarendon Press, Oxford, 1994.
[2] Jiří Adámek and Jiří Rosickỳ. Locally presentable and accessible categories, volume 189. Cambridge University Press, 1994.
[3] Gregory Arone and Michael Ching. Goodwillie calculus. In Handbook of homotopy theory, pages 1–38. Chapman and Hall/CRC, 2020.
[4] Michael Barr. Coalgebras over a commutative ring. Journal of Algebra, 32(3):600–610, 1974.
[5] Michael Barr. $*$ -autonomous categories and linear logic. Mathematical Structures in Computer Science, 1(2):159–178, 1991. doi:10.1017/S0960129500001274.
[6] Jon Beck. Distributive laws. In Seminar on Triples and Categorical Homology Theory, pages 119–140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg.
[7] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop on Computer Science Logic, pages 121–135. Springer, 1994.
[8] John D. Berman. Higher lawvere theories. Journal of Pure and Applied Algebra, 224(9):106362, 2020.
[9] Gavin M. Bierman. What is a categorical model of intuitionistic linear logic? In Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA, volume 902 of Lecture Notes in Computer Science, pages 78–93. Springer, 1995. doi:10.1007/BFB0014046.
[10] Pierre-Louis Curien. Operads, clones, and distributive laws. In Operads and universal algebra, pages 25–49. World Scientific, 2012.
[11] Valeria de Paiva. Categorical Semantics of Linear Logic for All, pages 181–192. Springer Netherlands, Dordrecht, 2014.
[12] Sanath Devalapurkar and Peter Haine. On the James and Hilton-Milnor splittings, and the metastable EHP sequence. Documenta Mathematica, 26:1423–1464, 2021.
[13] Eric Finster, Samuel Mimram, Maxime Lucas, and Thomas Seiller. A cartesian bicategory of polynomial functors in homotopy type theory. In Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, volume 351 of EPTCS, pages 67–83, 2021. doi:10.4204/EPTCS.351.5.
[14] Marcelo Fiore, Zeinab Galal, and Hugo Paquet. Stabilized profunctors and stable species of structures. Logical Methods in Computer Science, 20, 2024. doi:10.46298/LMCS-20(1:17)2024.
[15] Marcelo Fiore, Nicola Gambino, and Martin Hyland. Monoidal bicategories, differential linear logic, and analytic functors. Preprint, 2024. arXiv:2405.05774.
[16] Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society, 77(1):203–220, 2008.
[17] Grant A. Fraser. The semilattice tensor product of distributive lattices. Transactions of the American Mathematical Society, 217:183–194, 1976.
[18] Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical proceedings of the cambridge philosophical society, 154(1):153–192, 2013.
[19] David Gepner, Rune Haugseng, and Joachim Kock. $\infty$ -operads as analytic monads. International Mathematics Research Notices, 2022(16):12516–12624, 2022.
[20] Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1–101, 1987. doi:10.1016/0304-3975(87)90045-4.
[21] Jean-Yves Girard. Normal functors, power series and $\lambda$ -calculus. Annals of pure and applied logic, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5.
[22] Thomas G Goodwillie. Calculus III: Taylor series. Geometry & Topology, 7(2):645–711, 2003.
[23] Elies Harington and Samuel Mimram. Polynomials in homotopy type theory as a Kleisli category. In Proceedings of MFPS XL, volume 4 of Electronic Notes in Theoretical Informatics and Computer Science, 2024.
[24] Rune Haugseng. On (co) ends in $\infty$ -categories. Journal of Pure and Applied Algebra, 226(2):106819, 2022.
[25] Simon Henry and Nicholas J. Meadows. Higher theories and monads. Preprint, 2021. arXiv:2106.02706.
[26] Martin Hyland and Andrea Schalk. Abstract games for linear logic extended abstract. Electronic Notes in Theoretical Computer Science, 29:127–150, 1999.
[27] Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183–231, 2003. doi:10.1016/S0304-3975(01)00241-9.
[28] Bart Jacobs. Semantics of weakening and contraction. Annals of Pure and Applied Logic, 69(1):73–106, 1994. doi:10.1016/0168-0072(94)90020-5.
[29] André Joyal. Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175(1-3):207–222, 2002.
[30] William F. Keigher. Symmetric monoidal closed categories generated by commutative adjoint monads. Cahiers de topologie et géométrie différentielle, 19(3):269–293, 1978.
[31] Marie Kerjean. Weak topologies for linear logic. Logical Methods in Computer Science, 12, 2016. doi:10.2168/LMCS-12(1:3)2016.
[32] Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351–365, 2012.
[33] Joachim Kock, André Joyal, Michael Batanin, and Jean-François Mascari. Polynomial functors and opetopes. Advances in Mathematics, 224(6):2690–2737, 2010.
[34] Yves Lafont. Logiques, catégories et machines. PhD thesis, Université Paris 7, 1988.
[35] Jacob Lurie. Higher topos theory. Princeton University Press, 2009.
[36] Jacob Lurie. Higher algebra. Preprint, 2017. URL: https://people.math.harvard.edu/˜lurie/papers/HA.pdf.
[37] Jacob Lurie. Kerodon. https://kerodon.net, 2018.
[38] Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15–215, 2009.
[39] Paul-André Melliès and Nicolas Tabareau. Resource modalities in tensor logic. Annals of Pure and Applied Logic, 161(5):632–653, 2010. doi:10.1016/J.APAL.2009.07.018.
[40] Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, 28(7):1253–1286, 2018. doi:10.1017/S0960129516000426.
[41] Paul-André Melliès. Categorical models of linear logic revisited. Unpublished manuscript, 2003. URL: https://hal.science/hal-00154229.
[42] nLab authors. commutative algebraic theory. https://ncatlab.org/nlab/show/commutative+algebraic+theory, February 2025. Revision 39.
[43] nLab authors. Goodwillie calculus. https://ncatlab.org/nlab/show/Goodwillie+calculus#GoodwillieDerivativeOfExponentialModality, February 2025. Revision 68.
[44] Emily Riehl. Categorical homotopy theory, volume 24. Cambridge University Press, 2014.
[45] R. A. G. Seely. Linear logic, $\ast$ -autonomous categories and cofree coalgebras. In Categories in computer science and logic, Contemp. Math., pages 371–382. American Mathematical Society, 1989.
[46] Moss E. Sweedler. Hopf algebras, volume 44 of Mathematics lecture note series. W. A. Benjamin, 1969.
[47] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
[48] Benoît Valiron and Steve Zdancewic. Modeling simply-typed lambda calculi in the category of finite vector spaces. Scientific Annals of Computer Science, 24(2), 2014. doi:10.7561/SACS.2014.2.325.

Appendix A Appendix

A.1 Proof of Theorem 10

Lemma 37.

Given a symmetric monoidal presentable $\infty$ -category $\mathcal{C}$ such that the functor $A\otimes-:\mathcal{C}\to\mathcal{C}$ preserves small colimits for every object $A\in\mathcal{C}$ , the $\infty$ -category $\operatorname{Comon}(\mathcal{C})$ is accessible.

Proof.

To show that $\operatorname{Comon}(\mathcal{C})$ is accessible, we use [35, Thm 5.4.7.11] which, given a well-behaved ambient large $\infty$ -subcategory of $\operatorname{Cat}$ , provides sufficient conditions for the $\infty$ -category of sections of a (locally) cocartesian fibration $p:X\to S$ sending some distinguished morphisms in $S$ to $p$ -cocartesian morphisms in $X$ to be in this class. Here, we will take the $\infty$ -category $\operatorname{Coacc}$ of coaccessible $\infty$ -categories and coaccessible functors as ambient $\infty$ -category and we will consider $p:({\mathcal{C}}^{\textnormal{op}})^{\otimes}\to\operatorname{Fin}_{\ast}$ to be the monoidal structure of $\mathcal{C}$ with inert morphisms as distinguished ones, so that the $\infty$ -category of sections is precisely $\operatorname{Mon}({\mathcal{C}}^{\textnormal{op}})$ . We first need to show that $\operatorname{Coacc}$ satisfies the hypothesis of the theorem.

(a)

By [35, Prop 5.4.7.3], $\operatorname{Acc}$ admits small limits and the forgetful functor $\operatorname{Acc}\to\operatorname{Cat}$ preserves small limits. By duality (the equivalence $-^{\textnormal{op}}:\operatorname{Cat}\to\operatorname{Cat}$ restricts to an equivalence $\operatorname{Coacc}\simeq\operatorname{Acc}$ ), $\operatorname{Coacc}$ also has small limits and the functor $\operatorname{Coacc}\to\operatorname{Cat}$ preserves them.
(b)

Given a coaccessible $\infty$ -category ${\mathcal{A}}$ , we have $\operatorname{Fun}(\Delta^{1},{\mathcal{A}})^{\textnormal{op}}\simeq% \operatorname{Fun}(\Delta^{1},{\mathcal{A}}^{\textnormal{op}})$ (because $(\Delta^{1})^{\textnormal{op}}\simeq\Delta^{1}$ ), which is accessible by [35, Prop 5.4.4.3], and $\operatorname{Fun}(\Delta^{1},{\mathcal{A}})$ is coaccessible.
(c)

Given coaccessible $\infty$ -categories ${\mathcal{A}}$ and ${\mathcal{B}}$ , a functor $F:{\mathcal{A}}\to\operatorname{Fun}(\Delta^{1},{\mathcal{B}})$ is coaccessible if and only if the two functors ${\mathcal{A}}\to{\mathcal{B}}$ induced by restricting to the vertices of $\Delta^{1}$ are coaccessible. This is because coaccessibility is a limit-preservation property, and limits in functor $\infty$ -categories are computed pointwise [35, Cor 5.1.2.3].

We now show that the map $p:({\mathcal{C}}^{\textnormal{op}})^{\otimes}\to\operatorname{Fin}_{\ast}$ satisfies the hypotheses of the theorem.

(i)

By definition of being a symmetric monoidal $\infty$ -category, the functor $p:({\mathcal{C}}^{\textnormal{op}})^{\otimes}\to\operatorname{Fin}_{\ast}$ is a cocartesian fibration, and thus a categorical fibration and a locally cocartesian fibration.
(ii)

The fiber of $p$ over $[n]\in\operatorname{Fin}_{\ast}$ is isomorphic to $({\mathcal{C}}^{\textnormal{op}})^{n}$ , which is coaccessible because ${\mathcal{C}}^{\textnormal{op}}$ is coaccessible and by ˜a.
(iii)

Given a pointed map $f\in\operatorname{Hom}_{\operatorname{Fin}_{\ast}}([m],[n])$ , the induced functor $F({\mathcal{C}}^{\textnormal{op}})^{m}\to({\mathcal{C}}^{\textnormal{op}})^{n}$ induced by the monoidal structure on ${\mathcal{C}}^{\textnormal{op}}$ is opposite to the functor ${\mathcal{C}}^{m}\to{\mathcal{C}}^{n}$ induced by the monoidal structure on ${\mathcal{C}}$ . This latter functor is accessible by virtue of [36, Lem 3.2.3.4], so $F$ is coaccessible.

By [35, Thm 5.4.7.11], $\operatorname{Mon}({\mathcal{C}}^{\textnormal{op}})$ is thus coaccessible, so that $\operatorname{Comon}({\mathcal{C}})$ is accessible. $\hfill\blacktriangleleft$

A.2 Proof of Theorem 21

Proof of Theorem 21.

The proof follows the one of [36, Prop 4.8.4.2], but without the smallness assumption on the class of simplicial sets ${\mathcal{K}}$ . To keep track precisely of size issues, fix Grothendieck universes ${\mathcal{U}}_{0}\in{\mathcal{U}}_{1}\in{\mathcal{U}}_{2}$ . The $\infty$ -category $\operatorname{Cat_{cc}}$ is by definition the $\infty$ -category of ${\mathcal{U}}_{1}$ -small $\infty$ -categories that admit ${\mathcal{U}}_{0}$ -small colimits. Given a diagram $\chi:J\to\operatorname{Cat_{cc}}$ , proposition 4.8.4.2 of [36] guarantees that there exists ${\mathcal{U}}_{2}$ -small $\infty$ -category ${\mathcal{C}}$ which is a colimit of this diagram, with an explicit description given in the proof of [35, Prop 5.3.6.2]. We need to show that it is actually (essentially) ${\mathcal{U}}_{1}$ -small.

To construct the $\infty$ -category ${\mathcal{C}}$ , first take a colimit ${\mathcal{D}}$ of the composition $\chi\xrightarrow{\chi}\operatorname{Cat_{cc}}\to\operatorname{Cat}$ . Let $\widehat{\mathcal{D}}$ denote the $\infty$ -category of ${\mathcal{U}}_{1}$ -small presheaves on ${\mathcal{D}}$ , i.e. $\widehat{\mathcal{D}}$ is the ${\mathcal{U}}_{2}$ -small free cocompletion of ${\mathcal{D}}$ under ${\mathcal{U}}_{1}$ -small colimits. Then we need to “force” the cocones in $\widehat{\mathcal{D}}$ coming from colimiting cocones in the $\infty$ -category of the diagram $\chi$ to become coliming cocones. This is done by taking $S$ -local objects in $\widehat{\mathcal{D}}$ for a well-chosen class of morphisms $S$ , this defines a reflective subcategory $\begin{matrix}\includegraphics{dagpub-standalone-combined-2025-05-21-15-10-53-% page-22.pdf2svg.svg}\end{matrix}$ The $\infty$ -category ${\mathcal{C}}$ is finally obtained by considering the smallest full subcategory of $\mathbb{D}$ containing the image of ${\mathcal{D}}\hookrightarrow\widehat{\mathcal{D}}\xrightarrow{r}\mathbb{D}$ and closed under ${\mathcal{U}}_{0}$ -small colimits.

The $\infty$ -category $\widehat{{\mathcal{D}}}$ is locally ${\mathcal{U}}_{1}$ -small since it is a $\infty$ -category of ${\mathcal{U}}_{1}$ -small presheaves [35, Ex 5.4.1.8], so ${\mathcal{C}}$ is also locally ${\mathcal{U}}_{1}$ -small (as a full subcategory of a locally small $\infty$ -category). To show it is (essentially) ${\mathcal{U}}_{1}$ -small, it suffices to show that the set of equivalence classes of its objects is ${\mathcal{U}}_{1}$ -small. Write ${\mathcal{C}}_{0}$ for the image of the functor ${\mathcal{D}}\hookrightarrow\widehat{\mathcal{D}}\xrightarrow{r}\mathbb{D}$ . Since ${\mathcal{D}}$ is ${\mathcal{U}}_{1}$ -small, so is ${\mathcal{C}}_{0}$ . By definition, ${\mathcal{C}}$ is the smallest full subcategory of $\mathbb{D}$ containing ${\mathcal{C}}_{0}$ and closed under ${\mathcal{U}}_{0}$ -small colimits. We describe ${\mathcal{C}}$ more explicitly as the union of a monotonous sequence $({\mathcal{C}}_{\alpha})$ of subcategories of $\mathbb{D}$ , where $\alpha$ takes values in all ${\mathcal{U}}_{0}$ -small ordinals. When $\alpha=\alpha^{\prime}+1$ , define ${\mathcal{C}}_{\alpha}$ to be the the full subcategory of $\mathbb{D}$ on objects that are colimits of ${\mathcal{U}}_{0}$ -small diagrams in ${\mathcal{C}}_{\alpha^{\prime}}$ . When $\alpha=\lim\alpha_{i}$ , define ${\mathcal{C}}_{\alpha}$ to be the union of the ${\mathcal{C}}_{\alpha_{i}}$ . Write $\epsilon$ for the smallest ordinal of cardinality that of ${\mathcal{U}}_{0}$ . We claim that ${\mathcal{C}}={\mathcal{C}}_{\epsilon}$ . Clearly, every ${\mathcal{C}}_{\alpha}$ is a full subcategory of ${\mathcal{C}}$ . It thus suffices to show that ${\mathcal{C}}_{\epsilon}$ is closed under ${\mathcal{U}}_{0}$ -small colimits. Let $\xi:K\to{\mathcal{C}}_{\epsilon}$ a ${\mathcal{U}}_{0}$ -small diagram in ${\mathcal{C}}_{\epsilon}$ . Since $K$ is ${\mathcal{U}}_{0}$ -small, the colimit of $\xi$ belongs to ${\mathcal{C}}_{\alpha}$ for some $|K|<\alpha<\epsilon$ , and hence also belongs to ${\mathcal{C}}_{\epsilon}$ . This concludes the proof that $\operatorname{Cat_{cc}}$ admits ${\mathcal{U}}_{0}$ -small colimits.

To prove that the monoidal structure is compatible with colimits, it suffices to notice that $\operatorname{Cat_{cc}}$ is monoidal closed, i.e. the functor ${\mathcal{C}}\otimes-:\operatorname{Cat_{cc}}\to\operatorname{Cat_{cc}}$ has a right adjoint, given by $\operatorname{Fun}_{\text{cc}}$ [36, Rem 4.8.1.6], and that left adjoints preserve any existing colimits [35, Prop 5.2.3.5]. $\hfill\blacktriangleleft$

[bib.bib1] [1] Samson Abramsky and Achim Jung. Handbook of Logic in Computer Science, volume 3, chapter Domain theory, pages 1–168. Clarendon Press, Oxford, 1994.

[bib.bib2] [2] Jiří Adámek and Jiří Rosickỳ. Locally presentable and accessible categories, volume 189. Cambridge University Press, 1994.

[bib.bib3] [3] Gregory Arone and Michael Ching. Goodwillie calculus. In Handbook of homotopy theory, pages 1–38. Chapman and Hall/CRC, 2020.

[bib.bib4] [4] Michael Barr. Coalgebras over a commutative ring. Journal of Algebra, 32(3):600–610, 1974.

[bib.bib5] [5] Michael Barr. $*$ -autonomous categories and linear logic. Mathematical Structures in Computer Science, 1(2):159–178, 1991. doi:10.1017/S0960129500001274.

[bib.bib6] [6] Jon Beck. Distributive laws. In Seminar on Triples and Categorical Homology Theory, pages 119–140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg.

[bib.bib7] [7] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop on Computer Science Logic, pages 121–135. Springer, 1994.

[bib.bib8] [8] John D. Berman. Higher lawvere theories. Journal of Pure and Applied Algebra, 224(9):106362, 2020.

[bib.bib9] [9] Gavin M. Bierman. What is a categorical model of intuitionistic linear logic? In Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA, volume 902 of Lecture Notes in Computer Science, pages 78–93. Springer, 1995. doi:10.1007/BFB0014046.

[bib.bib10] [10] Pierre-Louis Curien. Operads, clones, and distributive laws. In Operads and universal algebra, pages 25–49. World Scientific, 2012.

[bib.bib11] [11] Valeria de Paiva. Categorical Semantics of Linear Logic for All, pages 181–192. Springer Netherlands, Dordrecht, 2014.

[bib.bib12] [12] Sanath Devalapurkar and Peter Haine. On the James and Hilton-Milnor splittings, and the metastable EHP sequence. Documenta Mathematica, 26:1423–1464, 2021.

[bib.bib13] [13] Eric Finster, Samuel Mimram, Maxime Lucas, and Thomas Seiller. A cartesian bicategory of polynomial functors in homotopy type theory. In Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, volume 351 of EPTCS, pages 67–83, 2021. doi:10.4204/EPTCS.351.5.

[bib.bib14] [14] Marcelo Fiore, Zeinab Galal, and Hugo Paquet. Stabilized profunctors and stable species of structures. Logical Methods in Computer Science, 20, 2024. doi:10.46298/LMCS-20(1:17)2024.

[bib.bib15] [15] Marcelo Fiore, Nicola Gambino, and Martin Hyland. Monoidal bicategories, differential linear logic, and analytic functors. Preprint, 2024. arXiv:2405.05774.

[bib.bib16] [16] Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society, 77(1):203–220, 2008.

[bib.bib17] [17] Grant A. Fraser. The semilattice tensor product of distributive lattices. Transactions of the American Mathematical Society, 217:183–194, 1976.

[bib.bib18] [18] Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical proceedings of the cambridge philosophical society, 154(1):153–192, 2013.

[bib.bib19] [19] David Gepner, Rune Haugseng, and Joachim Kock. $\infty$ -operads as analytic monads. International Mathematics Research Notices, 2022(16):12516–12624, 2022.

[bib.bib20] [20] Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1–101, 1987. doi:10.1016/0304-3975(87)90045-4.

[bib.bib21] [21] Jean-Yves Girard. Normal functors, power series and $\lambda$ -calculus. Annals of pure and applied logic, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5.

[bib.bib22] [22] Thomas G Goodwillie. Calculus III: Taylor series. Geometry & Topology, 7(2):645–711, 2003.

[bib.bib23] [23] Elies Harington and Samuel Mimram. Polynomials in homotopy type theory as a Kleisli category. In Proceedings of MFPS XL, volume 4 of Electronic Notes in Theoretical Informatics and Computer Science, 2024.

[bib.bib24] [24] Rune Haugseng. On (co) ends in $\infty$ -categories. Journal of Pure and Applied Algebra, 226(2):106819, 2022.

[bib.bib25] [25] Simon Henry and Nicholas J. Meadows. Higher theories and monads. Preprint, 2021. arXiv:2106.02706.

[bib.bib26] [26] Martin Hyland and Andrea Schalk. Abstract games for linear logic extended abstract. Electronic Notes in Theoretical Computer Science, 29:127–150, 1999.

[bib.bib27] [27] Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183–231, 2003. doi:10.1016/S0304-3975(01)00241-9.

[bib.bib28] [28] Bart Jacobs. Semantics of weakening and contraction. Annals of Pure and Applied Logic, 69(1):73–106, 1994. doi:10.1016/0168-0072(94)90020-5.

[bib.bib29] [29] André Joyal. Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175(1-3):207–222, 2002.

[bib.bib30] [30] William F. Keigher. Symmetric monoidal closed categories generated by commutative adjoint monads. Cahiers de topologie et géométrie différentielle, 19(3):269–293, 1978.

[bib.bib31] [31] Marie Kerjean. Weak topologies for linear logic. Logical Methods in Computer Science, 12, 2016. doi:10.2168/LMCS-12(1:3)2016.

[bib.bib32] [32] Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351–365, 2012.

[bib.bib33] [33] Joachim Kock, André Joyal, Michael Batanin, and Jean-François Mascari. Polynomial functors and opetopes. Advances in Mathematics, 224(6):2690–2737, 2010.

[bib.bib34] [34] Yves Lafont. Logiques, catégories et machines. PhD thesis, Université Paris 7, 1988.

[bib.bib35] [35] Jacob Lurie. Higher topos theory. Princeton University Press, 2009.

[bib.bib36] [36] Jacob Lurie. Higher algebra. Preprint, 2017. URL: https://people.math.harvard.edu/˜lurie/papers/HA.pdf.

[bib.bib37] [37] Jacob Lurie. Kerodon. https://kerodon.net, 2018.

[bib.bib38] [38] Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15–215, 2009.

[bib.bib39] [39] Paul-André Melliès and Nicolas Tabareau. Resource modalities in tensor logic. Annals of Pure and Applied Logic, 161(5):632–653, 2010. doi:10.1016/J.APAL.2009.07.018.

[bib.bib40] [40] Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, 28(7):1253–1286, 2018. doi:10.1017/S0960129516000426.

[bib.bib41] [41] Paul-André Melliès. Categorical models of linear logic revisited. Unpublished manuscript, 2003. URL: https://hal.science/hal-00154229.

[bib.bib42] [42] nLab authors. commutative algebraic theory. https://ncatlab.org/nlab/show/commutative+algebraic+theory, February 2025. Revision 39.

[bib.bib43] [43] nLab authors. Goodwillie calculus. https://ncatlab.org/nlab/show/Goodwillie+calculus#GoodwillieDerivativeOfExponentialModality, February 2025. Revision 68.

[bib.bib44] [44] Emily Riehl. Categorical homotopy theory, volume 24. Cambridge University Press, 2014.

[bib.bib45] [45] R. A. G. Seely. Linear logic, $\ast$ -autonomous categories and cofree coalgebras. In Categories in computer science and logic, Contemp. Math., pages 371–382. American Mathematical Society, 1989.

[bib.bib46] [46] Moss E. Sweedler. Hopf algebras, volume 44 of Mathematics lecture note series. W. A. Benjamin, 1969.

[bib.bib47] [47] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.

[bib.bib48] [48] Benoît Valiron and Steve Zdancewic. Modeling simply-typed lambda calculi in the category of finite vector spaces. Scientific Annals of Computer Science, 24(2), 2014. doi:10.7561/SACS.2014.2.325.

∞-Categorical Models of Linear Logic

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

DOI:

Event:

Editors:

Series and Publisher:

Introduction

Toward higher-dimensional models of linear logic.

∞-categories.

∞-categorical models of linear logic.

Plan of the paper.

1 ∞-categories

Simplicial sets.

∞-categories.

Adjunctions.

Symmetric monoidal ∞-categories.

Monads.

2 ∞-categorical models of linear logic

2.1 Linear-non-linear adjunctions

Definition 1.

▶ Remark 2.

Proposition 3.

Proof.

Seely categories.

Definition 4.

Proposition 5.

Linear categories.

Definition 6.

2.2 Lafont categories

Definition 7.

Proposition 8.

Proof.

Proposition 9.

Proof.

Theorem 10.

Proof of Theorem 10.

2.3 ∗-autonomous categories

Definition 11 (∗-autonomous ∞-category).

Proposition 12.

Proof.

Proposition 13.

Proof.

Lemma 14.

Proof.

3 Models of linear logic in 1-categories

3.1 Relational polynomials

3.2 Domains

3.3 Modules

4 Models in ∞-categories with colimits

∞-categorical domains.

Proposition 15.

Proof.

Theorem 16.

Proof.

▶ Remark 17.

∞-categorical relations.

Definition 18.

▶ Remark 19.

Proposition 20.

Proof.

Theorem 21.

Proof.

Lemma 22.

Proof.

Theorem 23.

▶ Remark 24.

▶ Remark 25.

Proof of Theorem 23.

▶ Remark 26.

5 Spectra

Definition 27.

Definition 28.

Theorem 29.

Theorem 30.

Theorem 31.

Proof.

▶ Remark 32.

$\infty$ -Categorical Models of Linear Logic

$\infty$ -categories.

$\infty$ -categorical models of linear logic.

1 $\infty$ -categories

$\infty$ -categories.

Symmetric monoidal $\infty$ -categories.

2 $\infty$ -categorical models of linear logic

$\blacktriangleright$ Remark 2.

2.3 $\ast$ -autonomous categories

Definition 11 ( $\ast$ -autonomous $\infty$ -category).

4 Models in $\infty$ -categories with colimits

$\infty$ -categorical domains.

$\blacktriangleright$ Remark 17.

$\infty$ -categorical relations.

$\blacktriangleright$ Remark 19.

$\blacktriangleright$ Remark 24.

$\blacktriangleright$ Remark 25.

$\blacktriangleright$ Remark 26.

$\blacktriangleright$ Remark 32.

$\blacktriangleright$ Remark 33.

$\blacktriangleright$ Remark 34.

$\blacktriangleright$ Remark 35.

$\blacktriangleright$ Remark 36.