3.1 A first attempt: the derivative of a stable function

In light of these definitions, and in view of the role of linearity in analysis and geometry, a natural question appeared to the author: is it possible to turn such a general stable morphism $t\in {\mathbf{Coh}}_{{!}_{\mathsf g}}(E,F)$ into a linear map by an operation similar to differentiation?

This question should be made a bit more precise and is actually twofold: given $x\in {\textrm {Cl}}({E})$ ,

• • can we define a coherence space $E_x$ of all possible “extensions” of $x$ , that is, such that for all $u\in {\textrm {Cl}}({E_x})$ , the set $x\cup u\in {\textrm {Cl}}({E})$ ;

• • and is there a linear $t'(x)\in {\textrm {Cl}}({{E_x}\multimap {F}})$ such that, for all $u\in {\textrm {Cl}}({E_x})$ , $\hat {t}(x)\cup {t'(x)}\cdot {u}$ exists, is a subset of $\hat {t}(x\cup u)$ and is the “best” possible approximation of that set by means of a linear map?

A natural tentative answer to the first question is to take $\left |{E_x}\right |=\{a'\in \left |{E}\right |\mid \forall a\in x\ a{\begin{smallmatrix}{\smallfrown }\\[-5pt]{\smallsmile }\end{smallmatrix}}_{E}a'\}$ (with $a_1{\begin{smallmatrix}{\smallfrown }\\[-5pt]{\smallsmile }\end{smallmatrix}}_{E_x}a_2$ if $a_1{\begin{smallmatrix}{\smallfrown }\\[-5pt]{\smallsmile }\end{smallmatrix}}_{E}a_2$ ) and then $t'(x)=\{(a',b)\in \left |{E_x}\right |\times \left |{F}\right | \mid \exists x_0\subseteq x\ (x_0\cup \{a'\},b)\in t\}$ .

This works quite well if we take $x=\emptyset$ , in that case $E_x=E$ and $t'(\emptyset )\in \mathbf{Coh}(E,F)$ and is characterized by

\begin{align*} {t'(\emptyset )}\cdot {u}=\bigcup _{a\in u}\hat {t}(\{a\}) \end{align*}

and notice also that we have a morphism $\overline {\mathsf{der}}_E=\{(a,\{a\})\mid a\in \left |{E}\right |\}\in \mathbf{Coh}(E,{!}_{\mathsf g} E)$ such that $t'(\emptyset )=t\,\overline {\mathsf{der}}_E$ .

Imagine now that $x=\{a,a'\}$ for some $a\smallfrown _{E}a'$ , and that moreover $t=\{(x,b)\}$ . Notice that $a,a'\in \left |{E_x}\right |$ . Then our definition of $t'(x)$ yields $(a,b),(a',b)\in t'(x)$ and hence $t'(x)\notin {\textrm {Cl}}({{E_x}\multimap {F}})$ . We stopped our investigation of this idea at this point in 1986-1987, but we could have tried to push this line of ideas a little bit further as we explain now.

We can interpret this failure as meaning that our definition of $E_x$ is not satisfactory, we can try $\left |{E_x}\right |=\{a'\in \left |{E}\right |\mid \forall a\in x\ a\smallfrown _{E}a'\}$ (with $a_1{\begin{smallmatrix}{\smallfrown }\\[-5pt]{\smallsmile }\end{smallmatrix}}_{E_x}a_2$ if $a_1{\begin{smallmatrix}{\smallfrown }\\[-5pt]{\smallsmile }\end{smallmatrix}}_{E}a_2$ ), that is, if $u\in {\textrm {Cl}}({E_x})$ , not only $x\cup u\in {\textrm {Cl}}({E})$ but also $x\cap u=\emptyset$ .

With this definition of $E_x$ , let $((a_i,b_i)\in t'(x))_{i=1,2}$ and assume that $a_1{\begin{smallmatrix}{\smallfrown }\\[-5pt]{\smallsmile }\end{smallmatrix}}_{E_x}a_2$ , that is $a_1{\begin{smallmatrix}{\smallfrown }\\[-5pt]{\smallsmile }\end{smallmatrix}}_{E}a_2$ . This means that there are $(x_i\subseteq x)_{i=1,2}$ with $((x_i\cup \{a_i\},b_i)\in t)_{i=1,2}$ , which implies $b_1{\begin{smallmatrix}{\smallfrown }\\[-5pt]{\smallsmile }\end{smallmatrix}}_{F}b_2$ because $x_1\cup x_2\cup \{a_1,a_2\}\in {\textrm {Cl}}({E})$ by definition of $E_x$ . If moreover $b_1=b_2$ , we know that $x_1\cup \{a_1\}=x_2\cup \{a_2\}$ which implies $a_1=a_2$ because $a_1\notin x_2$ and $a_2\notin x_1$ (remember that $x_1,x_2\subseteq x$ ). So we do have $t'(x)\in \mathbf{Coh}(E_x,F)$ . We can be even more precise: let $(a',b')\in t'(x)$ and let $b\in \hat {t}(x)$ , so that there is $x_0\subseteq x$ such that $(x_0,b)\in t$ . Let $x'_0\subseteq x$ be such that $(x'_0\cup \{a'\},b')\in t$ , then we have $x_0\smallfrown _{{!}_{\mathsf g} E}x'_0\cup \{a'\}$ because we know that $a'\notin x_0$ . Therefore $b\smallfrown _{F}b'$ and we have shown that $b'\in \left |{F_{\hat {t} (x)}}\right |$ from which it follows that $t'(x)\in \mathbf{Coh}(E_x,F_{\hat {t}(x)})$ .

Let us adopt the following convention introduced by Girard: given $(x_i\in {\textrm {Cl}}({E}))_{i\in I}$ , we use the notation $\sum _{i\in I}x_i$ to denote $\bigcup _{i\in I}x_i$ and to express at the same time that the $x_i$ ’s are pairwise disjoint and that $\bigcup _{i\in I}x_i\in {\textrm {Cl}}({X})$ . Then our definition of $t'(x)$ satisfies

\begin{align*} {t'(x)}\cdot {u}=\sum _{a\in u}(\hat {t}(x+\{a\})\setminus \hat {t}(x))\,. \end{align*}

Indeed, let first $b\in {t'(x)}\cdot {u}$ , so let $a\in u$ be such that $(a,b)\in t'(x)$ . There is $x_0\subseteq x$ such that $(x_0+\{a\},b)\in t$ from which it follows that $b\in \hat {t}(x+\{a\})$ . Next since $x_0+\{a\}$ is minimal such that $b\in \hat {t}(x_0+\{a\})$ and $a\notin x$ , we cannot have $b\in \hat {t}(x)$ from which the $\subseteq$ inclusion follows. Let now $b\in \sum _{a\in u}(\hat {t}(x+\{a\})\setminus \hat {t}(x))$ , so let $a\in u$ be such that $b\in \hat {t}(x+\{a\})\setminus \hat {t}(x)$ . Let $x'_0\subseteq x+\{a\}$ be such that $(x'_0,b)\in t$ . Since $b\notin \hat {t}(x)$ , we cannot have $x'_0\subseteq x$ and hence we must have $x'_0=x_0+\{a\}$ for some $x_0\subseteq x$ . Since $a\in u\in {\textrm {Cl}}({E_x})$ , we have $(a,b)\in t'(x)$ from which the $\supseteq$ inclusion follows.

This shows in particular that $\hat {t}(x)+{t'(x)}\cdot {u}\subseteq \hat {t}(x+u)$ . Let now $h\in \mathbf{Coh}(E_x,F_{\hat {t}(x)})$ be such that $\forall u\in {\textrm {Cl}}({E_x})\ \hat {t}(x)+{h}\cdot {u}\subseteq \hat {t}(x+u)$ , that is ${h}\cdot {u}\subseteq \hat {t}(x+u)\setminus \hat {t}(x)$ . In particular, for $u=\{a\}$ with $a\in \left |{E_x}\right |$ we get ${h}\cdot {\{a\}}\subseteq {t'(x)}\cdot {\{a\}}$ which means that $h\subseteq t'(x)$ . In that precise sense $t'(x)$ is the best linear under-approximation of the map $u\mapsto \hat {t}(x+u)\setminus \hat {t}(x)$ so can reasonably be called the derivative of $t$ at $x$ .

Let $s\in {\mathbf{Coh}}_{{!}_{\mathsf g}}(E,F)$ and $t\in {\mathbf{Coh}}_{{!}_{\mathsf g}}(F,G)$ so that $t\mathrel \circ s\in {\mathbf{Coh}}_{{!}_{\mathsf g}}(E,G)$ is the composition in the Kleisli category which can be described as follows:

\begin{multline*} t\mathrel \circ s =\{(x_1\cup \cdots \cup x_n,c)\in \left |{{!}_{\mathsf g} E}\right |\times \left |{G}\right | \mid \exists b_{1},\ldots ,b_{n}\in \left |{F}\right |\\ ((x_i,b_i)\in s)_{i=1}^n \text{ and } (\{b_{1},\ldots ,b_{n}\},c)\in t\} \end{multline*}

and is fully characterized by $\widehat {t\mathrel \circ s}(x)=\hat {t}(\widehat {s}(x))$ .

Remember that the coherence space ${1}\mathrel {\&}{1}$ has $\{(1,\ast ),(2,\ast )\}$ as web, with ${(1,\ast )}\smallfrown _{{1}\mathrel {\&}{1}}{(2,\ast )}$ . Let $s\in {\mathbf{Coh}}_{{!}_{\mathsf g}}(1,{1}\mathrel {\&}{1})$ and $t\in {\mathbf{Coh}}_{{!}_{\mathsf g}}({1}\mathrel {\&}{1},1)$ be given by

\begin{align*} s&=\{(\{\ast \},(1,\ast )),(\{\ast \},(2,\ast ))\}\\ t&=\{(\{(1,\ast ),(2,\ast )\},\ast )\}\,. \end{align*}

Then we have $t\mathrel \circ s=\{(\{\ast \},\ast )\}$ . Therefore, ${(t\mathrel \circ s)'(\emptyset )}\cdot {\{\ast \}}=\{\ast \}$ and on the other hand we have

\begin{align*} {t'(\widehat {s}(\emptyset ))}\cdot {({s'(\emptyset )}\cdot {\{\ast \}})} &={t'(\emptyset )}\cdot {({s'(\emptyset )}\cdot {\{\ast \}})}\\ &={t'(\emptyset )}\cdot {\{(1,\ast ),(2,\ast )\}}\\ &=\hat {t}\{(1,\ast )\}) \cup \hat {t}\{(2,\ast )\})\\ &=\emptyset \,. \end{align*}

This means that the chain rule

\begin{align*} (t\mathrel \circ s)'(x)=t'(s(x))\, s'(x) \end{align*}

does not hold for this differentiation of stable function, we only have a weak version thereof $(t\mathrel \circ s)'(x)\supseteq t'(s(x))\, s'(x)$ .

The reason for the failure of the chain rule is clear: the morphism $t$ is nonlinear (it needs to be fed with $\{(1,\ast ),(2,\ast )\}$ to output the atomic result $\ast$ , i.e., it uses its parameter at least twice) so in the computation of $\widehat {t\mathrel \circ s}(\{\ast \})$ , the atomic data $\ast$ is actually used at least twice, but this nonlinearity does not appear in $t\mathrel \circ s=\{(\{\ast \},\ast )\}$ , which turns out to be a linear morphism in $\mathbf{Coh}$ : the two used copies of $\ast$ have been “merged” because set union is an idempotent operation.

Another difficulty in this concrete approach to differentiation of stable maps is that it is not clear how to express the regularity (and hopefully, the stability) of the derivative $t'(x)$ with respect to $x$ (the author was not aware of the – at that time recently introduced – tangent categories of Rosický (Reference Rosický1984)), and therefore, it was unclear how to define higher derivatives in this kind of setting.

3.2 Coming back to differentiation in LL

In the early 2000’s, motivated by the phase space parameterized LL models of Bucciarelli and Ehrhard (Reference Bucciarelli and Ehrhard2001), the author explored categorical models of LL where formulas are interpreted as vector spaces and morphisms as linear maps (in the usual sense of Linear Algebra). In such categories, the only known resource modalities yield infinite dimensional vector spaces as soon as they are applied to a non $0$ space, and so the vector spaces under consideration must be equipped with a topology compatible with their algebraic structure. Two such models were developed by the author: Köthe sequence spaces Ehrhard (Reference Ehrhard2002) and finiteness spaces Ehrhard (Reference Ehrhard2005).

The objects of these models are topological vector spaces (tvs), which admit a simple description based on the existence of a “web” (in the sense of coherence spaces) which, in this algebraic context, can be understood as a Schauder basis, that is, not exactly a basis in the usual algebraic sense (Hamel basis), but a natural topological adaptation thereof, in which all the elements of the vector space can be written uniquely as possibly infinite linear combinations of base vectors (these infinite sums being defined as limits in the sense of the topology the vector space is endowed with). One important feature of these models is that webs are not used in the definition of morphisms, which are just linear and continuous maps.

The obtained categories $\mathcal{L}$ are models of $\mathsf {LL}$ such that the Kleisli category ${\mathcal{L}}_{{!}}$ can be described as a category of analytic (or more precisely entire) functions. Moreover, the homsets of these categories have a natural tvs structure (because $\mathcal{L}$ is a symmetric monoidal closed category) and in particular have an operation of addition: they are additive categories.

The fact that the morphisms of such CCCs ${\mathcal{L}}_{{!}}$ are analytic and therefore infinitely differentiable led to the idea of extending the typedFootnote ³ $\lambda$ -calculus with differential operations, developed in Ehrhard and Regnier (Reference Ehrhard and Regnier2003). The basic differential typing rule of this calculus is

\begin{equation*} \frac {\Gamma \vdash M:{A\Rightarrow B}\quad {\Gamma \vdash N :A}} {\Gamma \vdash {\mathsf{D} M\cdot N}:{A\Rightarrow B}} \end{equation*}

the intuition being that $A$ and $B$ denote some kind of tvs $E$ (of the symmetric monoidal closed category $\mathcal{L}$ ) and $F$ , and $M$ an entire function $f:E\rightarrow F$ , more precisely $f\in {\mathcal{L}}_{{!}}(E,F)$ (possibly depending on additional parameters listed in $\Gamma$ ). Such a function can be differentiated into another entire function $f'\in {\mathcal{L}}_{{!}}(E,{E}\multimap {F})$ such that, for any $x\in E$ , the map $u\mapsto f(x)+{f'(x)}\cdot {u}$ is the best affine approximation of the map $u\mapsto f(x+u)$ (in the sense of the topology our tvs are endowed with). Then, if $N$ denotes $u\in E$ , the term $\mathsf D{M}\cdot {N}$ denotes the analytic function $E\rightarrow F$ which maps $x$ to $f'(x)\cdot u$ . This slightly unusual writing of differentials makes it easy to iterate derivatives: given $({\Gamma }\vdash {N_i}:{A})_{i=1,2}$ , we have ${\Gamma }\vdash {\mathsf D{(\mathsf D{M}\cdot {N_1})}\cdot {N_2}}:{{A}\Rightarrow {B}}$ , the second derivative of $M$ , a bilinear morphism applied to its two linear arguments $N_1$ and $N_2$ .

This differential application induces a new redex, in the case where $M=\lambda x^{A}\,{P}$ with ${\Gamma ,x:A}\vdash {P}:{B}$ , similar to a $\beta$ -redex. The corresponding reduction is

\begin{align*} \mathsf D{(\lambda x^{A}\,{P})}\cdot {N}\mathrel {\rightarrow}\lambda x^{A}\,{\Big (\frac {\partial {P}}{\partial {x}}\cdot {N}\Big )} \end{align*}

where the term $\frac {\partial {P}}{\partial {x}}\cdot {N}$ is the differential substitution of $N$ for $x$ in $P$ , defined by induction on $P$ , which is typed as follows

\begin{align*} {\Gamma ,x:A}\vdash {\frac {\partial {P}}{\partial {x}}\cdot {N}}:{B} \end{align*}

which shows that, in the term $\frac {\partial {P}}{\partial {x}}\cdot {N}$ , the variable $x$ can still be free. This is due to the fact that in that term only one linear copy is substituted with $N$ . This linear substitution operation performs a nontrivial operation on $P$ , creating linear occurrences of $x$ to be substituted by $N$ on request. The most important case in the definition of $\frac {\partial {P}}{\partial {x}}\cdot {N}$ is when $P$ is an (ordinary) application $P=({Q}){R}$ with ${\Gamma ,x:A}\vdash {Q}:{{C}\Rightarrow {B}}$ and ${\Gamma ,x:A}\vdash {R}:{C}$ . The inductive definition of this linear substitution stipulates that

\begin{align*} \frac {\partial {({Q}){R}}}{\partial {x}}\cdot {N} =\Big ({\frac {\partial {Q}}{\partial {x}}\cdot {N}}\Big ){R}+\Big ({\mathsf D{Q}\cdot {\Big (\frac {\partial {R}}{\partial {x}}\cdot {N}\Big )}}\Big ){R} \end{align*}

and this definition involves the $+$ operation on terms, subject to the following typing rule

(1) \begin{equation} \frac {{\Gamma \vdash {M_1}:A}\quad {\Gamma \vdash {M_2}:A}} { \Gamma \vdash {M_1+M_2}:A} \end{equation}

(for each context $\Gamma$ and each type $A$ ) which has an obvious denotational interpretation in our tvs models and should, operationally, be understood as a nondeterministic superposition. The case of a variable is also interesting, we set

\begin{align*} \frac {\partial {y}}{\partial {x}}\cdot {N}= \begin{cases} N & \text{if }y=x\\ 0 & \text{otherwise} \end{cases} \end{align*}

where we see a $0$ which is the neutral element of the $+$ above. The meaning of this $0$ is that if $y\not =x$ , then “ $y$ does not depend on $x$ ” and so we are taking the derivative of a constant function; a more operational understanding is that $y$ has no linear occurrence of $x$ and hence the linear substitution fails. Addition is made possible by the typing rule (1) because the variable $x$ may have several potential linear occurrences in $P$ . Consider for instance $P=({x}){({x}){y}}$ typed as follows:

\begin{align*} {\Gamma ,y:A,x:{A}\Rightarrow {A}}\vdash {({x}){({x}){y}}}:{A} \end{align*}

and let $N$ be a term such that ${\Gamma }\vdash { }:{N}{{A}\Rightarrow {A}}$ , we have

\begin{align*} \frac {\partial {({x}){({x}){y}}}}{\partial {x}}\cdot {N} =({N}){({x}){y}}+({\mathsf D{x}\cdot {({N}){y}}}){({x}){y}} \end{align*}

where some intuitively clear equations on terms (such as $\mathsf D{M}\cdot {0}=0$ ) have been used implicitly. Let us write the term $P=({x_1}){({x_2}){y}}$ , using $x_1,x_2$ to distinguish the two occurrences of $x$ in $P$ . Only the occurrence $x_1$ is linear,Footnote ⁴ the occurrence $x_2$ is not because the occurrence $x_1$ might take as value a nonlinear function, using $x_2$ in a nonlinear way. This is why for substituting $N$ linearly for $x_2$ we need first to make the function $x_1$ use its argument linearly (or more precisely extract a linear copy of its argument); this is exactly the purpose of the $\mathsf D{x}\cdot {\_}$ in the second term of the sum.

It is worth observing that these differential reduction rules produce nontrivial sums even if the term we start from does not contain such sums. Consider for instance, in a typed calculus with a base type of booleans, the following term

\begin{align*} {x:\mathbf{Bool}}\vdash {M=\operatorname {\mathsf{if}}(x,\operatorname {\mathsf{if}}(x,\mathbf f,\mathbf t),\operatorname {\mathsf{if}}(x,\mathbf f,\mathbf t))}:{\mathbf{Bool}} \end{align*}

then the definition of differential substitution leads to the reduction

\begin{align*} ({\mathsf D{(\mathsf D{(\lambda x^{\mathbf{Bool}}\,{ }M)}\cdot {\mathbf t})}\cdot {\mathbf f}}){0} {\rightarrow}\mathbf t+\mathbf f\,. \end{align*}

This results from the fact that, using iterated differential application, we manage to give the variable $x$ two incompatible values $\mathbf t$ and $\mathbf f$ and the term $M$ is written in such a way that, when $x$ changes value during the computation (an impossible scenario in a deterministic setting), $M$ issues $\mathbf t$ or $\mathbf f$ , depending on the scheduling of this change of value. The order of the differential substitution being essentially irrelevant (this corresponds to the Schwarz rule of Calculus: the second derivative is a symmetric bilinear function), the computation is necessarily nondeterministic and leads to this nontrivial sum $\mathbf t+\mathbf f$ .

This kind of example strongly suggested that extending the $\lambda$ -calculus with differential constructs necessarily leads to essentially nondeterministic systems.

Later on, together with Laurent Regnier, the author developed a differential extension of LL in Ehrhard and Regnier (Reference Ehrhard and Regnier2004); Ehrhard (Reference Ehrhard2018), fully compatible with these semantic and syntactic ideas. The beauty of this differential LL is that the new differential logical structure does not require new connectives, but introduces new deduction rules relative to the resource modality $!$ of LL, dual to the standard rules of dereliction, weakening and contraction. We already mentioned codereliction $\overline {\mathsf{der}}_E$ in the setting of coherence spaces in Section 3.1; coweakening and cocontraction are similar (the first also exists in coherence spaces, the second not). The associated new cut elimination rules preserve this new symmetry. The recent paper Kerjean and Lemay (Reference Kerjean and Lemay2023) even extends this symmetry to promotion, the fundamentally infinitary rule of LL, which becomes then a bimonad.

5.1 Partial monoids

We first describe the kind of partial commutative monoids that our axiomatization of summability induces.

Thanks to that lemma, the following definition makes sense.

The proofs of these facts are standard and can also be found in Ehrhard (Reference Ehrhard2023b).

5.2 Summability structures

Let $\mathcal{L}$ be a category with zero-morphisms, that is, $\mathcal{L}$ is enriched over the category of pointed sets. We use $0_{X,Y}$ or simply $0$ for the distinguished zero-element of $\mathcal{L}(X,Y)$ , so that $f\, 0=0\, f=0$ . If $\mathcal{L}$ is a symmetric monoidal category (SMC), we also assume that ${0}\mathrel \otimes {f}=0$ and ${f}\mathrel \otimes {0}=0$ . If $\mathcal{L}$ has a terminal object $\top$ , notice that $\mathcal{L}(X,{\top })=\{0\}$ for any object $X$ .

The first structure we assume $\mathcal{L}$ to be equipped with is a functor ${\mathsf S}:\mathcal{L}\rightarrow\mathcal{L}$ whose intuitive meaning is to map any object $X$ to the object ${\mathsf S} X$ of all pairs $(x_0,x_1)$ of elements of $X$ for which the sum $x_0+x_1$ exists. In accordance with this intuition, this functor is equipped with three natural transformations $\operatorname {\pi }_{0},\operatorname {\pi }_{1},\sigma \in \mathcal{L}({\mathsf S} X,X)$ intuitively mapping such a pair to $x_0$ , $x_1$ and $x_0+x_1$ respectively.

Remember that the latter condition of Definition 4.4 means that if $f,g\in \mathcal{L}(Y,{\mathsf S} X)$ satisfy $(\operatorname {\pi }_{i}\, f=\operatorname {\pi }_{i}\, g)_{i=0,1}$ then $f=g$ ; this is the categorical way to say that ${\mathsf S} X$ is an object of pairs. From now on we fix a pre-summability structure on $\mathcal{L}$ .

The additional assumptions on pre-summability structures that we will introduce now for defining summability structures will turn each hom-set of $\mathcal{L}$ , equipped with $0$ and the operation “ $+$ ” defined above, into a partial commutative monoid in the sense of Section 5.2.

Proof. Since $\operatorname {\pi }_{0},\operatorname {\pi }_{1}\in \mathcal{L}({\mathsf S}^2 X,{\mathsf S} X)$ are summable, we know by Lemma 4.5 that $\operatorname {\pi }_{i}\,\operatorname {\pi }_{0},\operatorname {\pi }_{i}\,\operatorname {\pi }_{1}\in \mathcal{L}({\mathsf S}^2X,X)$ are summable for $i=0,1$ which gives us witnesses

\begin{equation*} (f_i =\langle\!\langle {\operatorname {\pi }_{i}\,\operatorname {\pi }_{0},\operatorname {\pi }_{i}\,\operatorname {\pi }_{1}}\rangle\!\rangle =({\mathsf S}\operatorname {\pi }_{i})\langle\!\langle {\operatorname {\pi }_{0},\operatorname {\pi }_{1}}\rangle\!\rangle ={\mathsf S}\operatorname {\pi }_{i}\in \mathcal{L}({\mathsf S}^2X,{\mathsf S} X))_{i=0,1}\,. \end{equation*}

We have $(\sigma \, f_i=\operatorname {\pi }_{i}\,\sigma _{{\mathsf S} X})_{i=0,1}$ by naturality of $\sigma$ so that $\sigma f_0$ and $\sigma f_1$ are summable by Lemma 4.5 again. So by 4.9 ( $\mathsf S$ -wit) the morphisms $f_0$ and $f_1$ are summable. We set

\begin{align*} \operatorname {\mathsf c}_X =\langle\!\langle {f_0,f_1}\rangle\!\rangle =\langle\!\langle {\langle\!\langle {\operatorname {\pi }_{0}\,\operatorname {\pi }_{0},\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}}\rangle\!\rangle , \langle\!\langle {\operatorname {\pi }_{1}\,\operatorname {\pi }_{0},\operatorname {\pi }_{1}\,\operatorname {\pi }_{1}}\rangle\!\rangle }\rangle\!\rangle =\langle\!\langle {{\mathsf S}\operatorname {\pi }_{0},{\mathsf S}\operatorname {\pi }_{1}}\rangle\!\rangle \,. \end{align*}

This definition implies immediately that $\operatorname {\pi }_{i}\,\operatorname {\pi }_{j}\,\operatorname {\mathsf c}_X=\operatorname {\pi }_{j}\,\operatorname {\pi }_{i}$ for all $i,j\in \{0,1\}$ and this characterizes $\operatorname {\mathsf c}_X$ by Lemma 4.4. One proves in the same way naturality, as well as the equation $\operatorname {\mathsf c}_X^2=\operatorname {\mathsf{Id}}_{{\mathsf S}^2X}$ .

Lemma 4.9. The following diagram commutes

Proof. For $i\in \{0,1\}$ , we have

\begin{align*} \operatorname {\pi }_{i}\,({\mathsf S}\sigma _X)\,\operatorname {\mathsf c}_X &=\sigma _X\,\operatorname {\pi }_{i}\,\operatorname {\mathsf c}_X \quad \text{by naturality of }\operatorname {\pi }_{i}\\ &=\sigma _X\,{\mathsf S}\operatorname {\pi }_{i} \quad \text{by definition of }\operatorname {\mathsf c}_X\\ &=\operatorname {\pi }_{i}\,\sigma _{{\mathsf S} X} \quad \text{by naturality of }\sigma \end{align*}

and the triangle commutes by joint monicity of the $\operatorname {\pi }_{i}$ ’s.

Now we use these properties of $\operatorname {\mathsf c}$ to prove associativity of our partially defined addition on $\mathcal{L}(X,Y)$ .

Proof. By 4.9 ( $\mathsf S$ -wit), the morphisms $\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle \in \mathcal{L}(X,{\mathsf S} Y)$ are summable; this summability has a witness $\langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \in \mathcal{L}(X,{\mathsf S}^2 Y)$ so that we can define

\begin{equation*} h=\operatorname {\mathsf c}_Y\,\langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \in \mathcal{L}(X,{\mathsf S}^2Y)\,. \end{equation*}

For $i\in \{0,1\}$ , let $h_i=\operatorname {\pi }_{i}\, h\in \mathcal{L}(X,{\mathsf S} Y)$ . We have $\operatorname {\pi }_{j}\, h_i =\operatorname {\pi }_{i}\,\operatorname {\pi }_{j}\, \langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle =f_{ji}$ and hence $f_{0i}$ and $f_{1i}$ are summable with $\langle\!\langle {f_{0i},f_{1i}}\rangle\!\rangle =h_i$ and sum

\begin{align*} f_{0i}+f_{1i} &=\sigma _Y\, h_i\\ &=\sigma _Y \,\operatorname {\pi }_{i}\operatorname {\mathsf c}_Y \,\langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \\ &=\sigma _Y\,({\mathsf S}\operatorname {\pi }_{i}) \,\langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \quad \text{by definition of }\operatorname {\mathsf c}_Y\\ &=\operatorname {\pi }_{i}\,\sigma _{{\mathsf S} Y} \,\langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \quad \text{ by naturality of }\sigma \end{align*}

so that $f_{00}+f_{10}$ and $f_{01}+f_{11}$ are summable with

\begin{align*} \langle\!\langle {f_{00}+f_{10},f_{01}+f_{11}}\rangle\!\rangle =\sigma _{{\mathsf S} Y} \,\langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \,. \end{align*}

We have

\begin{align*} (f_{00}+f_{10})+(f_{01}+f_{11}) &=\sigma _Y\,\sigma _{{\mathsf S} Y} \,\langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \\ &=\sigma _Y\,({\mathsf S}\sigma _Y) \,\langle\!\langle {\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle ,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \quad \text{by naturality of }\sigma \\ &=\sigma _Y \,\langle\!\langle {\sigma _Y\,\langle\!\langle {f_{00},f_{01}}\rangle\!\rangle , \sigma _Y\,\langle\!\langle {f_{10},f_{11}}\rangle\!\rangle }\rangle\!\rangle \quad \text{by Lemma 4.5}\\ &=\sigma _Y \,\langle\!\langle {f_{00}+f_{01},f_{10}+f_{11}}\rangle\!\rangle \\ &=(f_{00}+f_{01})+(f_{10}+f_{11})\,. \end{align*}

Proof. We have

\begin{align*} \operatorname {\pi }_{i}\,\operatorname {\pi }_{j}\,\operatorname {\mathsf c}_Y\,{\mathsf S}\langle\!\langle {f_0,f_1}\rangle\!\rangle &=\operatorname {\pi }_{j}\,\operatorname {\pi }_{i}\,{\mathsf S}\langle\!\langle {f_0,f_1}\rangle\!\rangle \\ &=\operatorname {\pi }_{j}\,\langle\!\langle {f_0,f_1}\rangle\!\rangle \,\operatorname {\pi }_{i} \quad \text{by naturality of }\operatorname {\pi }_{i}\\ &=f_j\,\operatorname {\pi }_{i}\\ &=\operatorname {\pi }_{i}\,{\mathsf S} f_j\\ &=\operatorname {\pi }_{i}\,\operatorname {\pi }_{j}\,\langle\!\langle {{\mathsf S} f_0,{\mathsf S} f_1}\rangle\!\rangle \end{align*}

which proves the first statement. The second follows easily from Lemma 4.5 using as usual the joint monicity of the $\operatorname {\pi }_{i}$ ’s.

In particular, we can speak of finite summable families of morphisms $\vec {f}=(f_i\in \mathcal{L}(X,Y))_{i\in I}$ and of their sum $\sum \vec {f}=\sum _{i\in I}f_i$ without particular cautions.

Theorem 4.3. If $(f_i\in \mathcal{L}(X,Y))_{i\in I}$ and $(g_j\in \mathcal{L}(Y,Z))_{j\in J}$ are finite summable families of morphisms, then the family $(g_j\, f_i\in \mathcal{L}(X,Z))_{(i,j)\in I\times J}$ is summable and

\begin{align*} \sum _{(i,j)\in I\times J}g_j\, f_i =\big (\sum _{j\in J}g_j\big )\,\big (\sum _{i\in I}f_i\big )\,. \end{align*}

5.3 The monad structure of $\mathsf S$

We assume that $\mathcal{L}$ is equipped with a summability structure, and we use the notations introduced above. By 4.8 ( $\mathsf S$ -zero) and 4.7 ( $\mathsf S$ -com), there are natural morphisms $(\operatorname {\iota }_{i}\in \mathcal{L}(X,{\mathsf S} X))_{i=0,1}$ given by $\operatorname {\iota }_{0}=\langle\!\langle {\operatorname {\mathsf{Id}}_X,0}\rangle\!\rangle$ and $\operatorname {\iota }_{1}=\langle\!\langle {0,\operatorname {\mathsf{Id}}_X}\rangle\!\rangle$ , and we have $\sigma \,\operatorname {\iota }_{i}=\operatorname {\mathsf{Id}}_X$ .

Proof. By Theorem 4.3, the family $(\operatorname {\pi }_{i}\,\operatorname {\pi }_{j})_{(i,j)\in \{0,1\}^2}$ is summable and hence by Lemma 4.2 the morphisms $\operatorname {\pi }_{0}\,\operatorname {\pi }_{0},\operatorname {\pi }_{0}\,\operatorname {\pi }_{1},\operatorname {\pi }_{1}\,\operatorname {\pi }_{0} \in \mathcal{L}({\mathsf S}^2X,X)$ are summable so that $\operatorname {\pi }_{0}\,\operatorname {\pi }_{0},\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}+\operatorname {\pi }_{1}\,\operatorname {\pi }_{0}$ are summable. We take $\operatorname {\tau }_X =\langle\!\langle {\operatorname {\pi }_{0}\,\operatorname {\pi }_{0},\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}+\operatorname {\pi }_{1}\,\operatorname {\pi }_{0}}\rangle\!\rangle$ . Let us prove for instance naturality, so let $f\in \mathcal{L}(X,Y)$ , we have

\begin{align*} \operatorname {\tau }_Y\,({\mathsf S}^2 f) &=\langle\!\langle {\operatorname {\pi }_{0}\,\operatorname {\pi }_{0},\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}+\operatorname {\pi }_{1}\,\operatorname {\pi }_{0}}\rangle\!\rangle \,({\mathsf S}^2 f)\\ &=\langle\!\langle {\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}\,({\mathsf S}^2 f), (\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}+\operatorname {\pi }_{1}\,\operatorname {\pi }_{0})\,({\mathsf S}^2 f)}\rangle\!\rangle \quad \text{by Lemma 4.5}\\ &=\langle\!\langle {\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}\,({\mathsf S}^2 f), \operatorname {\pi }_{0}\,\operatorname {\pi }_{1}\,({\mathsf S}^2 f) +\operatorname {\pi }_{1}\,\operatorname {\pi }_{0}\,({\mathsf S}^2 f))}\rangle\!\rangle \quad \text{by Lemma 4.5}\\ &=\langle\!\langle {f\,\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}, f\,\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}+f\,\operatorname {\pi }_{1}\,\operatorname {\pi }_{0}}\rangle\!\rangle \quad \text{by naturality of }\operatorname {\pi }_{0}\text{ and }\operatorname {\pi }_{1}\\ &=({\mathsf S} f)\,\langle\!\langle {\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}, \operatorname {\pi }_{0}\,\operatorname {\pi }_{1}+\operatorname {\pi }_{1}\,\operatorname {\pi }_{0}}\rangle\!\rangle \quad \text{by Lemma 4.5}\\ &=({\mathsf S} f)\,\operatorname {\tau }_X\,. \end{align*}

Last we have $\operatorname {\pi }_{0}\,\operatorname {\tau }_X\,\operatorname {\mathsf c}_X =\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}\,\operatorname {\mathsf c}_X =\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}=\operatorname {\pi }_{0}\,\operatorname {\tau }_X$ by definition of $\operatorname {\mathsf c}$ and

\begin{align*} \operatorname {\pi }_{1}\,\operatorname {\tau }_X\,\operatorname {\mathsf c}_X &=(\operatorname {\pi }_{1}\,\operatorname {\pi }_{0}+\operatorname {\pi }_{0}\,\operatorname {\pi }_{1})\,\operatorname {\mathsf c}_X\\ &=\operatorname {\pi }_{1}\,\operatorname {\pi }_{0}\,\operatorname {\mathsf c}_X+\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}\,\operatorname {\mathsf c}_X \quad \text{by Lemma 4.5}\\ &=\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}+\operatorname {\pi }_{1}\,\operatorname {\pi }_{0} \quad \text{by definition of }\operatorname {\mathsf c}\\ &=\operatorname {\pi }_{1}\,\operatorname {\tau }_X \quad \text{by Theorem 4.2}\,. \end{align*}

Proof. The monad commutations are easily checked, using as usual the joint monicity of the $\operatorname {\pi }_{i}$ ’s. For instance, one proves easily that

\begin{align*} ({\mathsf S}\operatorname {\tau }_X)\,\operatorname {\tau }_X &=\operatorname {\tau }_{{\mathsf S} X}\,\operatorname {\tau }_X\\ &=\langle\!\langle {\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}, \operatorname {\pi }_{1}\,\operatorname {\pi }_{0}\,\operatorname {\pi }_{0} +\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}\,\operatorname {\pi }_{0} +\operatorname {\pi }_{0}\,\operatorname {\pi }_{0}\,\operatorname {\pi }_{1}}\rangle\!\rangle \,. \end{align*}

Another important structure map of $\mathsf S$ was overlooked in Ehrhard (Reference Ehrhard2022).

Proof. We have $\operatorname {\iota }_{0}=\langle\!\langle {\operatorname {\mathsf{Id}}_X,0}\rangle\!\rangle$ and hence $\operatorname {\iota }_{0}\,\operatorname {\pi }_{0}=\langle\!\langle {\operatorname {\pi }_{0},0}\rangle\!\rangle \in \mathcal{L}({\mathsf S} X,{\mathsf S} X)$ and similarly $\operatorname {\iota }_{1}\,\operatorname {\pi }_{1}=\langle\!\langle {0,\operatorname {\pi }_{1}}\rangle\!\rangle \in \mathcal{L}({\mathsf S} X,{\mathsf S} X)$ . Therefore by 4.8 ( $\mathsf S$ -zero), we have $\sigma \,\operatorname {\iota }_{i}\,\operatorname {\pi }_{i}=\operatorname {\pi }_{i}$ for $i=0,1$ and since $\operatorname {\pi }_{0}$ and $\operatorname {\pi }_{1}$ are summable, 4.9 ( $\mathsf S$ -wit) implies that $\operatorname {\iota }_{0}\,\operatorname {\pi }_{0}$ and $\operatorname {\iota }_{1}\,\operatorname {\pi }_{1}$ are summable and we set

\begin{equation*} \mathsf l=\langle\!\langle {\operatorname {\iota }_{0}\,\operatorname {\pi }_{0},\operatorname {\iota }_{1}\,\operatorname {\pi }_{1}}\rangle\!\rangle \in \mathcal{L}({\mathsf S} X,{\mathsf S}^2X) \end{equation*}

which satisfies the announced condition.

5.4 Compatibility of the summability structure with the tensor product and the internal hom

We assume that $\mathcal{L}$ has an SMC structure, that is, a distinguished object $1$ (tensor unit) and a binary functor $\mathrel \otimes :\mathcal{L}^2\rightarrow\mathcal{L}$ (tensor product) together with natural isomorphisms $\lambda _X\in \mathcal{L}({1}\mathrel \otimes { }X,X)$ , $\rho _X\in \mathcal{L}({X}\mathrel \otimes {1},X)$ , $\alpha _{X_1,X_2,X_3}\in \mathcal{L}({({X_1}\mathrel \otimes {X_2})}\mathrel \otimes {X_3},{X_1}\mathrel \otimes {({X_2}\mathrel \otimes {X_3})})$ and $\gamma _{X_1,X_2}\in \mathcal{L}({X_1}\mathrel \otimes {X_2},{X_2}\mathrel \otimes {X_1})$ subject to the well-known Mac Lane coherence conditions.

Lemma 4.15. Let $\mathcal{L}$ be a summable SMC. There is a natural morphism

\begin{equation*} {\varphi }^1_{X_1,X_2} \in \mathcal{L}({{\mathsf S} X_1}\mathrel \otimes {X_2},{\mathsf S}({X_1}\mathrel \otimes {X_2})) \end{equation*}

such that $(\operatorname {\pi }_{i}\,{\varphi }^1={\operatorname {\pi }_{i}}\mathrel \otimes {X_2})_{i=0,1}$ .

Proof. We know that $\operatorname {\pi }_{0},\operatorname {\pi }_{1}\in \mathcal{L}({\mathsf S} X_1,X_1)$ are summable, so by 4.11 ( $\mathsf S$ - $\otimes$ ) the morphisms ${\operatorname {\pi }_{0}}\mathrel \otimes {X_2},{\operatorname {\pi }_{1}}\mathrel \otimes {X_2} \in \mathcal{L}({{\mathsf S} X_1}\mathrel \otimes {X_2},{X_1}\mathrel \otimes {X_2})$ are summable, we set ${\varphi }^1=\langle\!\langle {{\operatorname {\pi }_{0}}\mathrel \otimes {X_2},{\operatorname {\pi }_{1}}\mathrel \otimes {X_2}}\rangle\!\rangle$ . Let $(f_i\in \mathcal{L}(X_i,Y_i))_{i=1,2}$ , we have

\begin{align*} {\varphi }^1\,({{\mathsf S} f_1}\mathrel \otimes {f_2}) &=\langle\!\langle {({\operatorname {\pi }_{0}}\mathrel \otimes {X_2})\,({{\mathsf S} f_1}\mathrel \otimes {f_2}), ({\operatorname {\pi }_{1}}\mathrel \otimes {X_2})\,({{\mathsf S} f_1}\mathrel \otimes {f_2})}\rangle\!\rangle \quad \text{by Lemma 4.5}\\ &=\langle\!\langle {{f_1\,\operatorname {\pi }_{0}}\mathrel \otimes {f_2},{f_1\,\operatorname {\pi }_{1}}\mathrel \otimes {f_2}}\rangle\!\rangle \\ &={\mathsf S}({f_1}\mathrel \otimes {f_2})\,{\varphi }^1 \quad \text{by Lemma 4.5} \end{align*}

which shows that ${\varphi }^1$ is natural.

One defines ${\varphi }^2_{X_1,X_2} \in \mathcal{L}({X_1}\mathrel \otimes {{\mathsf S} X_2},{\mathsf S}({X_1}\mathrel \otimes {X_2}))$ by ${\varphi }^2_{X_1,X_2} =({\mathsf S}\gamma _{X_2,X_1})\,{\varphi }^1_{X_2,X_1}\gamma _{X_1,{\mathsf S} X_2}$ .

Theorem 4.5. The following diagrams commute

and hence $({\mathsf S},{\varphi }^1)$ is a commutative strong monad.

Proof. The diagrams are proven commutative using the joint monicity of the $\operatorname {\pi }_{i}$ ’s. Commutativity of the monad means that the following diagram commutes

which results from Lemma 4.12.

Remark 4.5. It is a standard fact that the common value $\widetilde {\varphi }_{X_1,X_2} =\operatorname {\tau }_{{X_1}\mathrel \otimes {X_2}} \,({\mathsf S}{\varphi }^1_{X_1,X_2}) \,{\varphi }^2_{{\mathsf S} X_1,X_2} =\operatorname {\tau }_{{X_1}\mathrel \otimes {X_2}} \,({\mathsf S}{\varphi }^2_{X_1,X_2}) \,{\varphi }^1_{X_1,{\mathsf S} X_2} \in \mathcal{L}({{\mathsf S} X_1}\mathrel \otimes {{\mathsf S} X_2},{\mathsf S}({X_1}\mathrel \otimes {X_2}))$ (and associated unit $\operatorname {\iota }_{0}\in \mathcal{L}(1,{\mathsf S}1)$ ) turns $\mathsf S$ into a lax monoidal monad. Notice that this morphism is characterized by

\begin{align*} \operatorname {\pi }_{0}\,\widetilde {\varphi } ={\operatorname {\pi }_{0}}\mathrel \otimes {\operatorname {\pi }_{0}}\quad \text{ and }\quad \operatorname {\pi }_{1}\,\widetilde {\varphi } ={\operatorname {\pi }_{1}}\mathrel \otimes {\operatorname {\pi }_{0}}+{\operatorname {\pi }_{0}}\mathrel \otimes {\operatorname {\pi }_{1}}\,. \end{align*}

If the SMC $\mathcal{L}$ is closed, with internal hom of $X$ and $Y$ denoted as $({X}\multimap {Y},\operatorname {\mathsf{ev}})$ where $\operatorname {\mathsf{ev}}\in \mathcal{L}({\left ({X}\multimap {Y}\right )}\mathrel \otimes {X},Y)$ is the evaluation morphism (and, given $f\in \mathcal{L}({Z}\mathrel \otimes {X},Y)$ , we use $\operatorname {\mathsf{cur}} f\in \mathcal{L}(Z,{X}\multimap {Y})$ for the currying of $f$ ), then we need a further assumption on the summability structure expressing that ${\mathsf S}{\left ({X}\multimap {Y}\right )}$ and ${X}\multimap {{\mathsf S} Y}$ are isomorphic. More precisely, notice that thanks to 4.11 ( $\mathsf S$ - $\otimes$ ) we have a morphism ${\varphi }_{X,Y}$ defined as the following composition of morphisms

so that ${\varphi }^{\mathord \multimap }_{X,Y} =\operatorname {\mathsf{cur}}{{\varphi }_{X,Y}}\in \mathcal{L}({\mathsf S}{\left ({X}\multimap {Y}\right )},{X}\multimap {{\mathsf S} Y})$ .

5.5 Summability in a cartesian category

We assume now that $\mathcal{L}$ is cartesian, that is, any finite family $(X_i)_{i\in I}$ has a cartesian product $(\mathop {\&}_{i\in I}X_i,(\mathsf{pr}_{i})_{i\in I})$ where the $\mathsf{pr}_{j}\in \mathcal{L}(\mathop {\&}_{i\in I}X_i,X_j)$ are the projections; we use $\top$ for the terminal object. When $(f_i\in \mathcal{L}(Y,X_i))_{i\in I}$ , we use $\langle {f_i}\rangle _{i\in I}$ for the unique morphism $Y\rightarrow\mathop {\&}_{i\in I}X_i$ which, post-composed with $\mathsf{pr}_{j}$ , yields $f_j$ .

In the sequel, when dealing with a (pre-)summability structure on a cartesian category, we always assume that 4.14 ( $\mathsf S$ - $\mathop {\&}$ ) holds.

5.6 Summability in the representable situation

It turns out that most nontrivial summability structures result from very simple properties of the category $\mathcal{L}$ that we describe now: such summability structures will be called representable.Footnote ⁶ We assume to be given an SMC category $\mathcal{L}$ with zero-morphisms which is cartesian.Footnote ⁷

We set $\mathbb D={1}\mathrel {\&}{1}$ , which will play a role similar to that of an object of infinitesimals in synthetic differential geometry Kock (Reference Kock2010); Cockett and Cruttwell (Reference Cockett and Cruttwell2014), see also Remark 4.12.

We assume that, for all objects $X$ of $\mathcal{L}$ , the internal hom $({\mathbb D}\multimap { }X,\operatorname {\mathsf{ev}})$ exists, where $\operatorname {\mathsf{ev}}\in \mathcal{L}({\left ({\mathbb D}\multimap { }\right )X}\mathrel \otimes {\mathbb D},X)$ is the evaluation morphisms. In that way we define a functor ${\mathsf S}=\left ({\mathbb D}\multimap {\_}\right ):\mathcal{L}\rightarrow\mathcal{L}$ . Since $\mathcal{L}$ has zero-morphisms, we can define $\overline {\pi }_{0}^{\&}=\langle {\operatorname {\mathsf{Id}}_1,0}\rangle$ , $\overline {\pi }_{1}^{\&}=\langle {0,\operatorname {\mathsf{Id}}_1}\rangle$ and $\Delta ^\&=\langle {\operatorname {\mathsf{Id}}_1,\operatorname {\mathsf{Id}}_1}\rangle$ which all belong to $\mathcal{L}(1,\mathbb D)$ . Notice that if $f\in \mathcal{L}(1,\mathbb D)$ , then ${f}\multimap {X}\in \mathcal{L}({\mathsf S} X,X)$ is a natural transformation.

In this pre-summability structure, saying that two morphisms $f_0,f_1\in \mathcal{L}(X,Y)$ are summable means that there is an $f\in \mathcal{L}({X}\mathrel \otimes {\mathbb D},Y)$ such that $f_i=f\,({\mathbb D}\mathrel \otimes {\overline {\pi }_{i}^{\&}})\,{\rho }^{-1}$ , and then we have $f_0+f_1=f\,({\mathbb D}\mathrel \otimes {\Delta ^\&})\,{\rho }^{-1}$ . We set $\langle\!\langle {f_0,f_1}\rangle\!\rangle ^{\mathord \otimes }=f$ , so that $\langle\!\langle {f_0,f_1}\rangle\!\rangle ={\operatorname {\mathsf{cur}}}\langle\!\langle {f_0,f_1}\rangle\!\rangle ^{\mathord \otimes }$ .

It is not particularly enlightening to unfold this definition and express directly the condition 4.9 ( $\mathsf S$ -wit) in terms of $\mathbb D$ , see Ehrhard (Reference Ehrhard2023b), beginning of Section 4 and more precisely Theorem 12.

▸ Example. 4.2. Another crucial example is that of probabilistic coherence space (PCS) introduced in Girard (Reference Girard, Ehrhard, Girard, Ruet and Scott2004); Danos and Ehrhard (Reference Danos and Ehrhard2011). A PCS is a pair $X=(\left |{X}\right |,\mathsf P{X})$ where $\left |{X}\right |$ is a set and $\mathsf P{X}\subseteq (\mathbb{R}_{\geq 0})^{\left |{X}\right |}$ that we consider as a poset (whose order relation is the product order) and that we assume to satisfy

• • $\mathsf P{X}$ is nonempty;

• • for all $a\in \left |{X}\right |$ , the set $\{x_a\mid x\in \mathsf P{X}\}\subseteq \mathbb{R}_{\geq 0}$ is bounded and is not reduced to $\{0\}$ ;

• • $\mathsf P{X}$ is down-closed (i.e., if $x\in \mathsf P{X}$ and $y\in (\mathbb{R}_{\geq 0})^{\left |{X}\right |}$ satisfy $y\leq x$ then $y\in \mathsf P{X}$ ) and closed under the lubs of monotone chains (i.e., if $(x(n)\in \mathsf P{X})_{n\in {\mathbb{N}}}$ is monotone for the pointwise order, then $(\!\sup _{n\in {\mathbb{N}}} x(n)_a)_{a\in \left |{X}\right |}\in \mathsf P{X}$ );

• • $\mathsf P{X}$ is closed under barycentric combinations, that is, if $x,y\in \mathsf P{X}$ and $p\in [0,1]$ , then $(1-p)x+py\in \mathsf P{X}$ (the algebraic operations being defined pointwise).

Remark 4.9. In the literature, the definition of PCSs is most often based on a duality typical of LL; the present definition is equivalent to the duality-based definition as shown in Girard (Reference Girard, Ehrhard, Girard, Ruet and Scott2004); Ehrhard (Reference Ehrhard2022), and is perhaps more intuitive. More precisely, given $\mathcal{P}\subseteq (\mathbb{R}_{\geq 0})^{I}$ for some set $I$ , we can define ${\mathcal{P}}^{\mathord \perp }=\{x'\in ({\mathbb{R}_{\geq 0}})^{ I}\mid \forall x \in {\mathcal{P}}\ \langle x,{x'}\rangle \leq 1\}\subseteq ({\mathbb{R}_{\geq 0}})^{I}$ where $\langle x,x'\rangle =\sum _{i\in I}x_ix'_i$ . Then, under the assumption that $\mathsf P{X}$ fulfills the two first conditions above, the two last conditions are equivalent to $\mathsf P{X}=\mathsf P{X}^{\bot \bot }$ .

A morphism from $X$ to $Y$ is a matrix $t\in (\mathbb{R}_{\geq 0})^{\left |{X}\right |\times \left |{Y}\right |}$ such that for all $x\in \mathsf P{X}$ , one has ${t}\cdot {x}\in \mathsf P{Y}$ where ${t}\cdot {x}=(\sum _{a\in \left |{X}\right |}t_{a,b}x_a)_{b\in \left |{Y}\right |}\in (\mathbb{R}_{\geq 0})^{\left |{Y}\right |}$ . These morphisms are in bijective correspondence with the functions $f:\mathsf P{X}\rightarrow\mathsf P{Y}$ which are monotone, commute with lubs of monotone sequences and satisfy $f((1-p)x+py)=(1-p)f(x)+pf(y)$ : given such an $f$ we define its matrix $t\in (\mathbb{R}_{\geq 0})^{\left |{X}\right |\times \left |{Y}\right |}$ as follows. Let $(a,b)\in \left |{X}\right |\times \left |{Y}\right |$ , then there is an ${\varepsilon }\in \mathbb{R}_{\gt 0}$ such that ${\varepsilon }\mathsf e_{a}\in \mathsf P{X}$ (where $\mathsf e_{a}\in (\mathbb{R}_{\geq 0})^{\left |{X}\right |}$ is defined by $(\mathsf e_{a})_{a'}=\boldsymbol{\delta }_{{a},{a'}}$ ), and we set $t_{a,b}={\varepsilon }^{-1} f({\varepsilon }\mathsf e_{a})_b$ , which does not depend on the choice of $\varepsilon$ . In that way, we have defined a category $\mathbf{Pcoh}$ where composition is defined by the usual product of matrices: if $s\in \mathbf{Pcoh}(X,Y)$ and $t\in \mathbf{Pcoh}(Y,Z)$ , then ${t}\,{s}\in \mathbf{Pcoh}(X,Z)$ is defined by $({t}\,{s})_{a,c}=\sum _{b\in \left |{Y}\right |}s_{a,b}t_{b,c}$ . The identity morphism $\operatorname {\mathsf{Id}}\in \mathbf{Pcoh}(X,X)$ is the diagonal matrix, $\operatorname {\mathsf{Id}}_{a,a'}=\boldsymbol{\delta }_{{a},{a'}}$ .

The category $\mathbf{Pcoh}$ is an SMC. The tensor unit is $1=(\{\ast \},[0,1])$ (upon identifying $(\mathbb{R}_{\geq 0})^{\{\ast \}}$ with $\mathbb{R}_{\geq 0}$ ). Given $(x(i)\in \mathsf P{X_i})_{i=1,2}$ , we set ${x(1)}\mathrel \otimes {x(2)} =(x(1)_{a_1}x(2)_{a_2})_{(a_1,a_2)\in \left |{X_1}\right |\times \left |{X_2}\right |} \in (\mathbb{R}_{\geq 0})^{\left |{X_1}\right |\times \left |{X_2}\right |}$ . We can define ${X_1}\mathrel \otimes {X_2}$ as $(\left |{X_1}\right |\times \left |{X_2}\right |,P)$ where $P$ is the least subset of $(\mathbb{R}_{\geq 0})^{\left |{X_1}\right |\times \left |{X_2}\right |}$ which contains all the ${x(1)}\mathrel \otimes {x(2)}$ for $(x(i)\in \mathsf P{X_i})_{i=1,2}$ and satisfies the two closure properties in the definition of PCS (the two last conditions). To describe more explicitly this operation, it is convenient to introduce the PCS ${X}\multimap {Y}=(\left |{X}\right |\times \left |{Y}\right |,Q)$ where $Q=\mathbf{Pcoh}(X,Y)$ . Then ${X}\multimap {1}$ is (trivially) isomorphic to the PCS $X^{\mathord \perp }$ where $\left |{X}\right |^{\mathord \perp }=\left |{X}\right |$ and $x'\in (\mathbb{R}_{\geq 0})^{\left |{X}\right |}$ belongs to $\mathsf{P}{{X}^{\mathord \perp }}$ if, for all $x\in \mathsf P{X}$ , one has $\langle x,x'\rangle =\sum _{a\in \left |{X}\right |}x_ax'_a\leq 1$ . It is then possible to prove that $X^{\bot \bot }=X$ (a kind of “bipolar theorem”, see Remark 4.9). Then one has ${X_1}{\mathrel \otimes }{X_2}={\left ({X_1}\multimap {{X_2}^{\mathord \perp }}\right )}^{\mathord \perp }$ and, based on this property, when equipped with $1$ and $\mathrel \otimes$ , the category $\mathbf{Pcoh}$ is an SMC. This SMC is closed with $({X}\multimap {Y},\operatorname {\mathsf{ev}})$ as internal hom from $X$ to $Y$ , with $\operatorname {\mathsf{ev}}_{((a,b),a'),b'}=\boldsymbol{\delta }_{{a},{a'}}\boldsymbol{\delta }_{{b},{b'}} \in \mathcal{L}({\left ({X}\multimap {Y}\right )}\mathrel \otimes {X},Y)$ as evaluation morphism, which satisfies of course ${\operatorname {\mathsf{ev}}}\cdot {({t}\mathrel \otimes {x})}={t}\cdot {x}$ for $t\in \mathbf{Pcoh}(X,Y)$ and $x\in \mathsf P{X}$ . This SMCC is even $\ast$ -autonomous with ${\mathord {\perp }}=1$ as dualizing object (this essentially boils down to the fact that $X^{\bot \bot }=X$ ).

The category $\mathbf{Pcoh}$ has all products: given a family $(X_i)_{i\in I}$ of PCSs, let $X$ be defined by $\left |{X}\right |=\bigcup _{i\in I}\{i\}\times \left |{X_i}\right |$ and $x\in (\mathbb{R}_{\geq 0})^{\left |{X}\right |}$ belongs to $\mathsf P{X}$ if $((x_{i,a})_{a\in \left |{X_i}\right |}\in \mathsf P{X_i})_{i\in I}$ . Equipped with $(\mathsf{pr}_{i}\in \mathbf{Pcoh}(X,X_i))_{i\in I}$ defined by $(\mathsf{pr}_{i})_{(j,a),a'}=\boldsymbol{\delta }_{{j},{i}}\boldsymbol{\delta }_{{a},{a'}}$ , $X$ is easily seen to be the cartesian product of the $X_i$ ’s, and we set $\mathop {\&}_{i\in I}X_i=X$ . Notice that $\mathsf P{(\mathop {\&}_{i\in I}X_i)}$ is isomorphic (for the order and for the barycentric structures) to $\prod _{i\in I}\mathsf P{X_i}$ . Given $(t_i\in \mathbf{Pcoh}(Y,X_i))_{i\in I}$ , the unique $\langle {t_i}\rangle _{i\in I}\in \mathbf{Pcoh}(Y,\mathop {\&}_{i\in I}X_i)$ such that $(\mathsf{pr}_{j}\,\langle {t_i}\rangle _{i\in I}=t_j)_{j\in I}$ is given by $(\langle {t_i}\rangle _{i\in I})_{b,(j,a)}=(t_j)_{b,a}$ for all $j\in I$ , $b\in \left |{Y}\right |$ and $a\in \left |{X_j}\right |$ .

The category $\mathbf{Pcoh}$ has zero morphisms (namely the $0$ matrix which obviously belongs to all homsets $\mathbf{Pcoh}(X,Y)$ ). The object $\mathbb D={1}\mathrel {\&}{1}$ is described by $\left |{\mathbb D}\right |=\{0,1\}$ and $\mathsf P{\mathbb D}=[0,1]^2$ (upon identifying $(\mathbb{R}_{\geq 0})^{\left |{\mathbb D}\right |}$ with $(\mathbb{R}_{\geq 0})^{2}$ ). Then $(\overline {\pi }_{0}^{\&},\overline {\pi }_{1}^{\&},\Delta ^\&\in \mathbf{Pcoh}(1,\mathbb D))$ are given by ${\overline {\pi }_{0}^{\&}}\cdot {u}=(u,0)$ , ${\overline {\pi }_{1}^{\&}}\cdot {u}=(0,u)$ and ${\Delta ^\&}\cdot { }u=(u,u)$ , for all $u\in [0,1]$ . Given a PCS $X$ , the PCS ${\mathsf S} X=\left ({\mathbb D}\multimap { }X\right )$ is given by $\left |{{\mathsf S} X}\right |=\{0,1\}\times \left |{X}\right |$ and an element of $\mathsf P{({\mathsf S} X)}$ is a $t\in (\mathbb{R}_{\geq 0})^{\{0,1\}\times \left |{X}\right |}$ such that ${t}\cdot {(\mathsf e_{0}+\mathsf e_{1})}\in \mathsf P{X}$ where $\mathsf e_{0}+\mathsf e_{1}\in \mathsf P{\mathbb D}$ corresponds to the pair $(1,1)\in [0,1]^2$ . In other words,

(2) \begin{align} \mathsf P{({\mathsf S} X)}\simeq \{(x(0),x(1))\in \mathsf P{X}^2\mid x(0)+x(1)\in \mathsf P{X}\} \end{align}

for the poset and barycentric structures. With this identification, the morphisms $\operatorname {\pi }_{0},\operatorname {\pi }_{1},\sigma \in \mathbf{Pcoh}({\mathsf S} X,X)$ are characterized by ${\operatorname {\pi }_{i}}\cdot {(x(0),x(1))}=x(i)$ and ${\sigma }\cdot {(x(0),x(1))}=x(0)+x(1)$ . It follows easily from these observations that two morphisms $t(0),t(1)\in \mathbf{Pcoh}(Y,X)$ are summable iff $\forall y\in \mathsf P{Y}\ {t(0)}\cdot {y}+{t(1)}\cdot {y}\in \mathsf P{X}$ , and the corresponding witness $\langle\!\langle {t(0),t(1)}\rangle\!\rangle \in \mathbf{Pcoh}(Y,{\mathsf S} X)$ is given as a matrix by $\langle\!\langle {t(0),t(1)}\rangle\!\rangle _{b,(i,a)}=t(i)_{b,a}$ and characterized by ${\langle\!\langle {t(0),t(1)}\rangle\!\rangle }\cdot {y}=({t(0)}\cdot {y},{t(1)}\cdot {y})$ if we consider Equation (2) as an equality. From this characterization of summability and witnesses, it follows easily that $\mathbf{Pcoh}$ is a representably summable category.

We know by Theorem 4.4 that $\mathsf S$ has a canonical (bi)monad structure. In the representable situation, we can describe more directly this structure by means of a (bi)monoid structure on $\mathbb D$ . We describe first the comonoid structure.

Proof. Clearly $\overline {\pi }_{0}^{\&},\overline {\pi }_{1}^{\&}\in \mathcal{L}(1,\mathbb D)$ are summable (with $\langle\!\langle {\overline {\pi }_{0}^{\&},\overline {\pi }_{1}^{\&}}\rangle\!\rangle ^{\mathord \otimes }=\operatorname {\mathsf{Id}}_{\mathbb D}$ and $\overline {\pi }_{0}^{\&}+\overline {\pi }_{1}^{\&}=\Delta ^\&$ ). So by Lemma 4.14 the morphisms $({\overline {\pi }_{i}^{\&}}\mathrel \otimes {\overline {\pi }_{j}^{\&}} \in \mathcal{L}({1}\mathrel \otimes {1},{\mathbb D}\mathrel \otimes {\mathbb D}))_{(i,j)\in \{0,1\}^2}$ are summable. By Lemma 4.2, the morphisms ${\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}$ , ${\overline {\pi }_{1}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}$ and ${\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{1}^{\&}}$ are summable, and hence the morphisms ${\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}$ and ${\overline {\pi }_{1}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}+{\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{1}^{\&}}$ are summable. This gives us a witness $\langle\!\langle {{\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}, {\overline {\pi }_{1}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}+{\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{1}^{\&}}}\rangle\!\rangle ^{\mathord \otimes } \in \mathcal{L}({{1}\mathrel \otimes {1}}\mathrel \otimes {\mathbb D},{\mathbb D}\mathrel \otimes {\mathbb D})$ and we set

\begin{equation*} \overline {\operatorname {\tau }} =\langle\!\langle {{\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}, {\overline {\pi }_{1}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}+{\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{1}^{\&}}}\rangle\!\rangle ^{\mathord \otimes } \,{\lambda }^{-1}\,{\lambda }^{-1} \in \mathcal{L}(\mathbb D,{\mathbb D}\mathrel \otimes {\mathbb D}) \end{equation*}

which obviously satisfies the announced equations. Uniqueness results from the joint epicity of $\overline {\pi }_{0}^{\&}$ and $\overline {\pi }_{1}^{\&}$ . The fact that we define in that way a commutative comonoid is easily checked, again by joint epicity of $\overline {\pi }_{0}^{\&}$ and $\overline {\pi }_{1}^{\&}$ . For instance (keeping the associator $\alpha$ implicit), the morphism $\overline {\operatorname {\tau }}^{(3)} =({\overline {\operatorname {\tau }}}\mathrel \otimes {\mathbb D})\,\overline {\operatorname {\tau }} =({\mathbb D}\mathrel \otimes {\overline {\operatorname {\tau }}})\,\overline {\operatorname {\tau }} \in \mathcal{L}(\mathbb D,{\mathbb D}\mathrel \otimes {{\mathbb D}\mathrel \otimes {\mathbb D}})$ is characterized by $\overline {\operatorname {\tau }}^{(3)}\,\overline {\pi }_{0}^{\&}={\overline {\pi }_{0}^{\&}}\mathrel \otimes {{\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}}$ and $\overline {\operatorname {\tau }}^{(3)}\,\overline {\pi }_{1}^{\&} ={\overline {\pi }_{1}^{\&}}\mathrel \otimes {{\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}} +{\overline {\pi }_{0}^{\&}}\mathrel \otimes {{\overline {\pi }_{1}^{\&}}\mathrel \otimes {\overline {\pi }_{0}^{\&}}} +{\overline {\pi }_{0}^{\&}}\mathrel \otimes {{\overline {\pi }_{0}^{\&}}\mathrel \otimes {\overline {\pi }_{1}^{\&}}}$ . The commutations involving the counit $\mathsf{pr}_{0}$ result from the fact that $\mathsf{pr}_{i}\,\overline {\pi }_{j}^{\&}=\boldsymbol{\delta }_{{i},{j}}\operatorname {\mathsf{Id}}_1$ .

Proof. Remember that $\mathbb D={1}\mathrel {\&}{1}$ , so we can set $\overline {\mathsf{l}} =\langle {\lambda _1\,({\mathsf{pr}_{0}}\mathrel \otimes {\mathsf{pr}_{0}}), \lambda _1\,({\mathsf{pr}_{1}}\mathrel \otimes {\mathsf{pr}_{1}})}\rangle$ which obviously satisfies the announced property, which characterizes $\overline {\mathsf{l}}$ uniquely by Lemma 4.18. The fact that we define in that way a commutative monoid is easy to check. For instance (keeping implicit the associator $\alpha$ and the $\lambda$ isos) we have $\overline {\mathsf{l}}^{(3)} =\overline {\mathsf{l}}\,({\overline {\mathsf{l}}}\mathrel \otimes {\mathbb D}) =\overline {\mathsf{l}}\,({\mathbb D}\mathrel \otimes {\overline {\mathsf{l}}}) =\langle {\mathsf{pr}_{0}\mathrel \otimes \mathsf{pr}_{0}\mathrel \otimes \mathsf{pr}_{0},\mathsf{pr}_{1}\mathrel \otimes \mathsf{pr}_{1}\mathrel \otimes \mathsf{pr}_{1}}\rangle \in \mathcal{L}(\mathbb D\mathrel \otimes \mathbb D\mathrel \otimes \mathbb D,\mathbb D)$ . The commutations of the diagram involving the unit $\Delta ^\&$ result from the fact that $\mathsf{pr}_{i}\,\Delta ^\&=\operatorname {\mathsf{Id}}_1$ for $i=0,1$ . The last statement means that the following diagrams commute

where $\gamma _{2,3}$ is the Mac Lane iso which exchanges the 2 central factors of the $4$ -fold tensor product. The first diagram obviously commutes. For the second we use Lemma 4.18. We have

\begin{align*} \overline {\operatorname {\tau }}\,\overline {\mathsf{l}}\,({\overline {\pi }_{i}^{\&}}\mathrel \otimes {\overline {\pi }_{j}^{\&}}) &=\overline {\operatorname {\tau }} \,\boldsymbol{\delta }_{{i},{j}}\overline {\pi }_{i}^{\&}\\ &=\boldsymbol{\delta }_{{i},{j}}\sum _{\genfrac {}{}{0pt}{1}{(l,r)\in \{0,1\}^2}{l+r=i}} {\overline {\pi }_{l}^{\&}}\mathrel \otimes {\overline {\pi }_{r}^{\&}} \end{align*}

and

\begin{align*} ({\overline {\mathsf{l}}}\mathrel \otimes {\overline {\mathsf{l}}}) \,\gamma _{2,3} \,({\overline {\operatorname {\tau }}}\mathrel \otimes {\overline {\operatorname {\tau }}}) \,({\overline {\pi }_{i}^{\&}}\mathrel \otimes {\overline {\pi }_{j}^{\&}}) &=({\overline {\mathsf{l}}}\mathrel \otimes {\overline {\mathsf{l}}}) \,\gamma _{2,3} \,\Big ({\Big (\sum \limits _{\genfrac {}{}{0pt}{1}{(l,r)\in \{0,1\}^2}{l+r=i}} {\overline {\pi }_{l}^{\&}}\mathrel \otimes {\overline {\pi }_{r}^{\&}}\Big )}\mathrel \otimes { }\Big ) {\big (\sum \limits _{\genfrac {}{}{0pt}{1}{(l',r')\in \{0,1\}^2}{l'+r'=j}} {\overline {\pi }_{l}^{\&}}\mathrel \otimes {\overline {\pi }_{r}^{\&}}\big )}\\ &=({\overline {\mathsf{l}}}\mathrel \otimes {\overline {\mathsf{l}}}) \,\gamma _{2,3} \, \sum \limits _{\genfrac {}{}{0pt}{1}{(l,r,l',r')\in \{0,1\}^4}{l+r=i,\ l'+r'=j}} \overline {\pi }_{l}^{\&}\mathrel \otimes \overline {\pi }_{r}^{\&}\mathrel \otimes \overline {\pi }_{l'}^{\&}\mathrel \otimes \overline {\pi }_{r'}^{\&}\\ &=({\overline {\mathsf{l}}}\mathrel \otimes {\overline {\mathsf{l}}}) \, \sum \limits _{\genfrac {}{}{0pt}{1}{(l,r,l',r')\in \{0,1\}^4}{l+r=i,\ l'+r'=j}} \overline {\pi }_{l}^{\&}\mathrel \otimes \overline {\pi }_{l'}^{\&}\mathrel \otimes \overline {\pi }_{r}^{\&}\mathrel \otimes \overline {\pi }_{r'}^{\&}\\ &=\sum \limits _{\genfrac {}{}{0pt}{1}{(l,r,l',r')\in \{0,1\}^4}{l+r=i,\ l'+r'=j}} \boldsymbol{\delta }_{{l},{l'}}\boldsymbol{\delta }_{{r},{r'}} \overline {\pi }_{l}^{\&}\mathrel \otimes \overline {\pi }_{r}^{\&}\\ &=\boldsymbol{\delta }_{{i},{j}}\sum \limits _{\genfrac {}{}{0pt}{1}{(l,r)\in \{0,1\}^2}{l+r=i}} {\overline {\pi }_{l}^{\&}}\mathrel \otimes {\overline {\pi }_{r}^{\&}} \end{align*}

Then it can be checked that the bimonad structure of $\mathsf S$ is induced by this bimonoid structure of $\mathbb D$ : the unit of the monad is $\operatorname {\iota }_{0}=\left ({\mathsf{pr}_{0}}\multimap {X}\right )\in \mathcal{L}({\mathsf S} X,X)$ (identifying $X$ and ${1}\multimap { }X$ ) and its multiplication is $\operatorname {\tau }=\left ({\overline {\operatorname {\tau }}}\multimap { }X\right )\in \mathcal{L}({\mathsf S} X,{\mathsf S}^2 X)$ (identifying ${{\mathbb D}\mathrel \otimes {\mathbb D}}\multimap {X}$ and ${\mathsf S}^2X=\left ({\mathbb D}\multimap {\left ({\mathbb D}\multimap { }X\right )}\right )$ which are canonically isomorphic). The comonad structure of $\mathsf S$ can be described similarly using the unit $\Delta ^\&$ and the product $\overline {\mathsf{l}}$ of the monoid structure of $\mathbb D$ . The distributive law of the bimonad, which is the flip isomorphism $\operatorname {\mathsf c}_X\in \mathcal{L}({\mathsf S}^2X,{\mathsf S}^2X)$ , is obtained similarly from the braiding of the SMC structure of $\mathcal{L}$ : $\operatorname {\mathsf c}_X=\left ({\gamma _{\mathbb D,\mathbb D}}\multimap {X}\right )$ (leaving again implicit the canonical iso between ${{\mathbb D}\mathrel \otimes {\mathbb D}}\multimap {X}$ and ${\mathsf S}^2X$ ).