We develop further the theory of monoidal bicategories by introducing and studying bicategorical counterparts of the notions of a linear explonential comonad, as considered in the study of linear logic, and of a codereliction transformation, introduced to study differential linear logic via differential categories. As an application, we extend the differential calculus of
Joyal's analytic functors to analytic functors between presheaf categories, just as ordinary calculus extends from a
single variable to many variables.

Marcelo Fiore
Department of Computer Science and Technology, University of Cambridge

Nicola Gambino
Department of Mathematics, University of Manchester

Martin Hyland
Department of Pure Mathematics and Mathematical Statistics, University of Cambridge

18N10, 18M45, 18F40, 18D60, 18M80.

§ INTRODUCTION

§.§ Context and motivation

The aim of this paper is to develop  and connect two apparently distant strands of research: low-dimensional category theory and differential linear logic. Let us begin by providing some context and motivation for our work.

By low-dimensional category theory we mean here the study of two-dimensional and  three-dimensional, categories  [6, 57] and  [42, 45] respectively. The subject has grown enourmously in the last decades, with motivation coming both from within category theory itself and from other parts of mathematics. Indeed, just as it is useful to study standard set-based mathematical structures (such as groups and vector spaces) by assembling them into categories, it is natural to investigate category-based mathematical structures (monoidal categories and Grothendieck toposes) by forming appropriate two-dimensional categories (see [8] for example), and so on. Furthermore, low-dimensional categorical structures find applications in algebra, algebraic topology, topological quantum field theory, to obtain more informative invariants for mathematical objects (knots), via the research programme known as categorification [5]. One of the key advances
in this area has been the development of the theory of monoidal bicategories, initiated by Kapranov and Voevodsky in [59, 60] and continued by many others, in [10, 12, 18, 23, 28, 44, 41].  This promises to serve a role as important as that of monoidal categories, in the study of topological quantum field theories,  [58, 73].

The other area involved in this paper is differential linear logic, introduced by Ehrhard and Reignier in [27, 29], as an extension of the linear logic, introduced by Girard in [39].
The subject arose from the observation that many models of linear logic, such those based on categories of topological vector spaces [26], possess a well-behaved notion of differentiation. Remarkably, not only  is it possible to introduce a syntactic counterpart of it, but the idea leads to interesting applications to the $\lambda$-calculus, obtained by introducing a Taylor series expansion for $\lambda$-terms [30].

The study of differential linear logic led also to the introduction of differential categories [3, 4], which provide categorical models of differential linear logic.
Since  differential categories axiomatise the essential categorical structure required to have a well-behaved operation of differentiation on the maps of a category, they have a wide range of examples across various areas of mathematics.
Their axioms are formulated on top of those for a categorical model of linear logic, which is given by symmetric monoidal categories $(\catE, \otimes, \unit)$ equipped with a linear exponential comonad $\bang(-) \co \catE \to \catE$,  a symmetric monoidal comonad satisfying some additional axioms [64]. In this setting, we think of maps $f \co A \to B$ as being `linear' and of Kleisli maps $f \co \bang A \to B$ as being `non-linear'.  Following the idea that the derivative of a function is a function in two arguments, linear in one and non-linear in the other, the derivative of a map $f \co \bang A \to B$ in a differential category has the form $\mathrm{d} F \co A \otimes \bang A \to B$. In the presence of sufficient structure on the ambient category, this operation is equivalent to having a natural transformation, referred to either as a codereliction transformation [3, 27]
or a creation map [34] in the literature, with components of the form $\coder_A \co A \to \bang A$, and subject to a few axioms. Remarkably, these axioms allow us to derive counterparts of all the
basic results on differentiation [3].

Here, we apply the idea of categorification to the study of models of linear logic and differential linear logic and contribute to developing a new theory, unavoidably more subtle and complex than the existing one, based on symmetric monoidal bicategories. This is of interest for logic and theoretical computer science since the additional layer of structure present in bicategories, namely 2-cells (morphisms between morphisms), can be used to model computational rewriting steps between terms [69, 71].

The origin of this line of investigation can be traced back to categorifications of the relational model of linear logic [19]. Recall that the relational model arises by considering the monad on the category of sets and functions whose algebras are commutative monoids and extending it to a monad on the category of sets and relations, written $\Rel$ here. The duality available on $\Rel$ allows us to turn this monad into a comonad $\bang(-) \co \Rel \to \Rel$, which can then be shown to satisfy all the axioms for a linear exponential comonad, so that its Kleisli category is cartesian closed.

$\Set$     $\Cat$
$\Rel$     $\Prof$

Free commutative monoid
$\wn(-)\co \Set \to \Set$
Free symmetric strict monoidal category
$\wn(-) \co \Cat \to \Cat$
Linear exponential

comonad $\bang(-) \co \Rel \to \Rel$
Linear exponential

pseudocomonad $\bang(-) \co \Prof \to \Prof$

Kleisli category $\Kl{\Rel}$

Kleisli bicategory $\Kl{\Prof}$
The relational model and its categorification.

These ideas were categorified in [19] by replacing sets with small categories and relations with profunctors, also known as distributors or bimodules [6, 7]. As typical  in the process of categorification, there is now additional freedom, since there are several 2-monads on the 2-category of small categories and functors, written $\Cat$ here, that may be considered to take the place of the monad for commutative monoids.

An example of particular interest, illustrated in <ref>, arises by considering the 2-monad on $\Cat$ whose strict algebras are symmetric strict monoidal categories. This 2-monad extends to a pseudomonad
on $\Prof$ by a form of pseudodistributivity [32],
which can then be turned into a pseudocomonad by duality, as before.
The associated Kleisli bicategory, called the bicategory of categorical symmetric sequences here,
and written $\Sym$, was originally introduced in [31], where it was shown to be cartesian closed. This bicategory was investigated further in connection with the theory of operads in [40], and shown to admit rich additional structure in [36, 38].

The distinction between linear and non-linear maps acquires particular significance in this example: a linear map here is a map $F \co A \to B$ in $\Prof$, a functor
$F \co B^\op \times A \to \Set$. Such a functor $F$ determines canonically a functor $F^\dag\co \pshA \to \pshB$ between presheaf categories, defined by an coend formula which is reminiscent of the expression for the linear map associated to a matrix:

\[
F^\dag(X,a) = \int^{a \in A} F[b, a] \times X(a) \mathrlap{.}
\]

By contrast, a non-linear map is a map $F \co  A \to B$ in $\Sym$, a profunctor $F \co \bang A \to B$.
Such a profunctor $F$ induces a functor $F^\ddag \co \pshA \to \pshB$ between presheaf categories,
defined by a formula similar to the one for the
Taylor series expansion of an analytic function:

\[
F^\ddag(X,b) = \int^{\alpha \in \bang A} F[b, \alpha] \times X^{\alpha} \mathrlap{.}
\]

(Here, $X^{\alpha} = X(a_1) \times \ldots \times X(a_n)$, for $X \in \pshA$ and $\alpha = \langle a_1, \ldots, a_n \rangle \in \bang A$.)
We call such functors analytic since they generalise the the analytic functors on $\Set$ introduced by Joyal in [52] as part of his approach to enumerative combinatorics [9, 51].
(Joyal's analytic functors arise when $A = B = \mathsf{1}$.)

These ideas led to  a new line of research, outlined in [48], aimed at extending theory and examples of categorical models to linear logic to the two-dimensional setting. This provides a so-called `quantitative semantics' for a variety of logical systems which are of interest also in theoretical computer science,  [35, 33, 50, 67, 68, 76, 77].

The first goal of this paper is to establish the analogy between the relational and profunctor models on a more precise basis, by  developing a bicategorical counterpart of the standard theory of models of linear logic, which recovers the results on profunctors as a special case. The motivation for creating such a theory can readily be seen by observing that, while many facts about the relational model follow from the theory of linear exponential comonads, analogous results in the two-dimensional context have been proved on a case-by-case basis. While some first steps towards a bicategorical theory have been taken recently [35, 50, 66, 67], much foundational work remains to be done. Here, we address this issue by considering counterparts of some key notions
and results on models of linear logic, in particular those related to the notion of a linear exponential comonad considered in [47].

The second goal of this work is to provide a bicategorical counterpart of a special class of differential categories [3, 4] and show that the bicategory of profunctors is an example of this new notion.
The motivation for this is twofold. On the one hand we wish to make precise the analogy with the relational model of differential linear logic; on the other hand, we wish to provide a clean approach to extending the differential calculus for analytic functors on $\Set$ developed in [52] to analytic functors between presheaf categories, analogously to how calculus in a single variable extends to many variables,
or one has of differentiation in the different context of polynomial functors [1].
To the best of our knowledge, this is the first example of a genuinely two-dimensional model of differential linear logic.

§.§ Main contributions

Our first main contribution is the definition and study of the notion of a linear exponential pseudocomonad, which we introduce in <ref> as a bicategorical counterpart of the notion of a linear exponential comonad  in [47]. We support this definition by generalising several facts about one-dimensional models of linear logic to the two-dimensional setting.  We then prove results (<ref> and <ref>) that help us to construct linear exponential pseudocomonads in many cases of interest, including in our application to the bicategory of profunctors.

Our second main contribution is the exploration of consequences of the assumption of additional structure and properties on the ambient bicategory, offering a modular development of the theory.  In particular, under the additional assumption of existence of finite products, we construct the so-called Seely equivalences and show that they provide the structure of a sylleptic strong monoidal 2-functor (<ref>). Because of coherence issues, a direct approach seems daunting. We therefore offer a more conceptual treatment, inspired by a passing remark in [37], which allows us to handle all coherence in an efficient way. Overall, we prove bicategorical counterparts of all the diagrams considered in [27] and  [34], starting from our notion of linear exponential pseudocomonad.

The third main contribution of this paper is the definition of a bicategorical counterpart of the codereliction transformation, given in <ref>, which provides one possible way of definition a derivation operation. The definition of a codereliction transformation considered here is a two-dimensional version of the one considered in [34]. While the notion considered therein (under the name of creation map) is equivalent to the one considered in the context of differential categories in the one-dimensional setting, as shown in [3],  it offers some advantages when transported to the two-dimensional setting since, as discussed below, it allows us to deal effectively with coherence issues. In order to do this, we work under additional assumptions, including that the ambient bicategory $\catK$ has biproducts and that the induced convolution structure is a coproduct. These hold in our application.

Finally, we show that the bicategory of categorical symmetric sequences admits a codereliction (<ref>), which allows us to extend the derivative operation to analytic functors between presheaf categories. To achieve this result, we show that the pseudomonad obtained by extending to $\Prof$ the free symmetric strict monoidal category 2-monad on $\Cat$ is a linear exponential pseudocomonad in our sense (<ref>) and that the additional hypotheses underpinning our definition of a codereliction transformation are satisfied (<ref>).
This then determines the desired operation of differentiation for analytic functors between presheaf categories.

§.§ Technical aspects
The development of the paper involved overcoming a number of conceptual and technical challenges. First of all, the bicategorical definitions underpinning the subject are rather complex, as they involve a significant amount of data and a large number of coherence conditions. Because of this, extending results from the one-dimensional to the two-dimensional setting involves a combination of trivial and non-trivial aspects. While it is generally possible to guess what the desired statements are, their proofs usually  require long calculations. A good illustration of this point that can be found in the existing literature is the statement that a bicategory with finite products admits a canonical symmetric monoidal structure, with tensor product given by binary products <cit.>. Thankfully, known strictification theorems help us to reduce the complexity of the notions that we need to use, while maintaining sufficient generality to cover the intended examples.

Issues of coherence had to be faced also when introducing our key notions, that of a linear exponential pseudocomonad and that of a codereliction transformation. For the former, we are able to arrive at a definition for which coherence axioms are completely determined by the fundamental notions in the theory of monoidal bicategories by taking the definition in [47] as our starting point.
It has been pleasing to observe how the coherence conditions for these notions are exactly what is required to prove the desired facts, which we hope provides corroboration for the robustness of the coherence conditions in [23]. Given the troubled evolution of coherence in monoidal bicategories (see  <cit.> and <cit.> for some details), we believe this experience is helpful for the future development of the theory.

The definition of a codereliction presented additional problems, in that it is not known whether its axioms can be expressed purely in terms of the basic concepts of the theory of monoidal categories. For this reason, if  we were to require the presence of invertible 2-cells in the diagrams that are part of the definition of a codereliction transformation in [3], we would then be facing the question of what coherence axioms to impose on them, which appears to be a difficult question.  To resolve this problem, we develop a careful analysis  by first showing that the diagrams
expressing the axioms for a codereliction transformation in [34] (under the name of a creation map) are  filled by canonical 2-cells. The definition of a codereliction transformation can then be simply stated as requiring these 2-cells to be invertible, thus sidestepping any issue of coherence. We hope that our results provide guidance for the formulation of coherence conditions in the future. It should also be pointed out that, since our approach uses non-invertible 2-cells in a crucial way, it is not immediately subsumed by the theory of $(\infty, 1)$-categories, although it may be possible to develop an $(\infty, 2)$-categorical counterpart of it.

§.§.§ Outline of the paper
<ref> reviews the basic definitions and theorems of the theory of monoidal bicategories that will be needed in the paper. In <ref> we study symmetric pseudocomonoids in
a symmetric monoidal bicategory. We introduce and study linear exponential pseudocomonads in <ref> and compare our notion with  the one introduced in [50].

We explore our definitions further  under the assumption in <ref> that the ambient bicategory has finite products and in <ref> that it has finite biproducts. We introduce our bicategorical notion of codereliction in <ref>. We conclude the paper in <ref> by showing how the bicategory of analytic functors can be equipped with a codereliction operator, thereby modelling differential linear logic.

§.§.§ References and conventions.
In order to keep the paper at a reasonable length and avoid duplication of material that is now standard, we refer to [10, 23, 44] for the coherence conditions of the notions that we use.  Many of our proofs will construct the relevant 2-cells and indicate how to prove the required coherence conditions in text. This is similar to how standard diagram-chasing arguments are outlined in one-dimensional category theory. Readers who wish to fill in the details of the proofs are advised to keep the references above at hand.  For differential linear logic and differential categories, our main references are [3, 27, 34]. The notation for differential linear logic and differential categories used here follows closely that in [27], as summarised in <ref>.

\begin{align*}
\text{Weakening} & \quad \weak_A \co \bang A \to \unit  &
\text{Coweakening} &  \quad  \coweak_A \co \unit \to  \bang A \\
\text{Contraction} & \quad  \con_A \co  \bang A  \to  \bang A \otimes \bang A   &
\text{Cocontraction} & \quad  \cocon_A \co \bang A \otimes \bang A \to \bang A \\
\text{Dereliction} & \quad  \der_A \co \bang A \to A   &
\text{Codereliction} & \quad  \coder_A \co  A \to \bang A \\
\text{Promotion} & \quad \dig_A \co \bang A  \to \bbang A &
\end{align*}

The structural maps.

§.§.§ Acknowledgements
Nicola Gambino acknowledges that this material is based upon work supported by the US Air Force Office for Scientific Research under award number FA9550-21-1-0007 and by EPSRC via grant EP/V002325/2. Marcelo Fiore acknowledges that this material is based upon work supported by EPSRC via grant EP/V002309/1. Nicola Gambino wishes to thank Zeinab Galal, Adrian Miranda and Federico Olimpieri for
helpful discussions.

§ PRELIMINARIES

We assume that readers are familiar with the key notions of two-dimensional category theory [54, 62]. Bicategories will be denoted with letters $\catK, \catL, \ldots$. When working with a bicategory $\catK$, we use upper-case letters $A, B, C, \ldots$ for objects, lower-case letters $f \co A \to B$, $g \co B \to C, \ldots$ for maps, and lower-case Greek letters $\alpha \co f \Rightarrow f'$ for 2-cells. Composition is written simply by juxtaposition and the identity map on $A \in \catK$ is written $\id_A \co A \to A$.  If $f \co A \to B$ is an adjoint equivalence in $\catK$, we write
$f^\bullet \co B \to A$ for its adjoint.

When we say that a bicategory $\catK$ has finite products (or finite coproducts), this is intended in the bicategorical sense [75], even when $\catK$ is a 2-category. For binary products, this means that for every $A, B \in \catK$, we have an object $A \with B \in \catK$ and projections  $\pi_1 \co A \with B \to A$ and $\pi_2 \co A \with B \to B$ which are universal, for every $X \in \catK$, composition with $\pi_1$ and $\pi_2$ induces an adjoint equivalence

\[
\begin{tikzcd}
\catK[X, A \with B] \ar[r, "(  \pi_1(-) {,} \pi_2 (-))"]  &[8ex] \catK[X,A] \times \catK[A, B] \mathrlap{.}
\end{tikzcd}
\]

The terminal object is denoted $\top$. The diagonal map of an object $A \in \catK$ is written $\Delta_A \co A \to A \with A$. If $\catK$ has finite coproducts, we write $A + B$ for the coproduct of $A, B \in \catK$, and $\iota_1 \co A \to A + B $ and $\iota_2 \co B \to A + B$ for the coprojections. The initial object is denoted $0$. The codiagonal map of an object $A \in \catK$ is written $\nabla_A \co A + A \to A$.

If $\catK$ and $\catL$ are bicategories with finite products and $F \co \catK \to \catL$ is a pseudofunctor,
we say that $F$ preserves finite products if  the canonical maps
$F(A \with B) \to FA \with FB$, for $A, B \in \catK$,
and $F(\term) \to \term$ are equivalences. We adopt this definition also when $\catK$ and $\catL$
are 2-categories and $F$ is a 2-functor. We do not spell out the corresponding definition for coproducts.

§.§ Monoidal bicategories and Gray monoids
Recall from <cit.> the strictification theorem for bicategories, asserting that every bicategory is biequivalent to a 2-category.
This result gives as a scholium the strictification theorem for monoidal categories, asserting that every monoidal category is equivalent to a strict one,
since a monoidal category is a bicategory with a single object and a strict monoidal category is a 2-category with a single object.

A similar pattern arises one dimension up, with tricategories and Gray-categories, defined as in [42, 45], replacing bicategories and 2-categories, respectively.
The strictification theorem for tricategories asserts that every tricategory is triequivalent to a Gray-category,  <cit.> and <cit.>.
This gives a strictification result for monoidal bicategories since a monoidal bicategory is a tricategory with a single object and a Gray monoid is a Gray-category with a single
object <cit.>. Below, we recall some of this material.
The notion of a Gray monoid is recalled in <ref> using the notion of a cubical pseudofunctor in <cit.> or <cit.>, and then partially unfolded.

A Gray monoid is a 2-category $\catK$ equipped with

* a cubical pseudofunctor $(\arghole) \otimes (=) \co \catK \times \catK \to \catK$, called the tensor product,

* an object $\unit \in \catK$, called the unit,

which satisfy the associativity and unit conditions strictly.

Let $\catK$ be a Gray monoid.[We refer to a Gray monoid by its underlying 2-category if this does not cause confusion.
An analogous convention is adopted for other kinds of structures throughout the paper.]
Recall that part of the pseudofunctoriality for the tensor product
involves, a natural isomorphism whose components are invertible 2-cells

\[
\begin{tikzcd}[column sep = large]
A \otimes B \ar[d,"\id_A \otimes g"']\ar[dr,phantom,"\Two\phi_{f,g}"]\ar[r,"f \otimes \id_B"] & A' \otimes B \ar[d,"\id_{A'} \otimes g"] \\
A \otimes B' \ar[r,"f \otimes \id_{B'}"'] & A' \otimes B' \mathrlap{,}
\end{tikzcd}
\]

where $f \co A \to A'$ and $g \co B \to B'$, subject to appropriate compatibility conditions <cit.>. As in [23], we take $f \otimes g \co A \otimes B \to A' \otimes B'$ to be the composite

\[
\begin{tikzcd}
A \otimes B \ar[r, "\id_{A} \otimes g" ] &
A' \otimes B \ar[r, "f \otimes \id_{B'}"] &
A' \otimes B' \mathrlap{.}
\end{tikzcd}
\]

We adopt an analogous convention to define $\alpha \otimes \beta \co f \otimes g \to f' \otimes g'$ for $\alpha \co f \Rightarrow f'$ and $\beta \co g \Rightarrow g'$. The other choice is canonically isomorphic and we shall often suppress mention of  these isomorphisms for brevity, since they are essentially unique [24, 25].
Note that the associativity and unit axioms hold strictly and so in particular $A \otimes (B \otimes C) = (A \otimes B) \otimes C$ for every $A, B, C \in \catK$, and $A \otimes  \unit  = A =  \unit \otimes A$ for all $A \in \catK$.

In preparation for the material on linear exponential pseudocomonads in <ref>, we recall the notions of a lax monoidal pseudofunctor, monoidal pseudonatural transformation, and monoidal modification. Here, a lax monoidal pseudofunctor is what is called a weak monoidal homomorphism in <cit.>.

Let $\catK$ and $\catL$ be Gray monoids. A lax monoidal pseudofunctor from $\catK$ to $\catL$ is a pseudofunctor $F \co \catK \to \catL$ equipped with

* a pseudonatural transformation with components on objects $\monn_{A, B} \co FA \otimes FB \to F(A \otimes B)$, for $A, B \in \catK$,

* a map $\moni \co  \unit \to F( \unit)$,

* an invertible modification with components

\[
\begin{tikzcd}[column sep=huge]
FA \otimes FB \otimes FC \ar[d,"\monn_{A,B} \otimes \id_{FC}"']\ar[dr,phantom,"\Two\omega_{A,B,C}"]\ar[r,"\id_{FA} \otimes \monn_{B,C}"] & FA \otimes F(B \otimes C) \ar[d,"\monn_{A, B \otimes C}"] \\
F(A  \otimes B) \otimes FC  \ar[r,"\monn_{A \otimes B, C}"'] & F(A \otimes B \otimes C)
\mathrlap{,}
\end{tikzcd}
\]

for $A, B, C \in \catK$, which we call the associativity constraint of $F$,

* two invertible modifications with components

\[
\begin{tikzcd}[column sep = tiny]
F  \unit \otimes FA
\ar[d, phantom, description, "\Two \zeta_A"]
\ar[dr, "\monn_{\unit, A}"]   &
\\
\unit \otimes FA
\ar[ur, "\moni \otimes \id_{FA}"]
\ar[rr, "\id_{FA}"']  &
\phantom{} &
FA \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}[column sep = tiny]
FA \otimes F  \unit
\ar[d, phantom, description, "\Two \kappa_A"]
\ar[dr, "\monn_{A,  \unit}"]   &
\\
FA \otimes \unit
\ar[ur, "\id_{FA} \otimes \moni"]
\ar[rr, "\id_{FA}"']  &
\phantom{} &
FA \mathrlap{,}
\end{tikzcd}
\]

for $A, B \in \catK$, which we call the left and right unitality constraints of $F$,

which satisfy the two coherence conditions in <cit.>.

We say that $F$ is a strong monoidal if the components of $\monn$ and  $\moni$ are equivalences in $\catL$.

Let $F, G \co \catK \to \catL$ be lax monoidal pseudofunctors. A monoidal pseudonatural transformation from $F$ to $G$ is a
pseudonatural transformation $p \co F \Rightarrow G$  equipped with

* an invertible modification with components

\[
\begin{tikzcd}[column sep = large]
FA \otimes FB \ar[d, "p_A \otimes p_B"'] \ar[r, "\monn_{A,B}"] \ar[dr,phantom,"\Two p^2_{A,B}"] & F(A \otimes B) \ar[d, "p_{A\otimes B}"]  \\
GA \otimes GB \ar[r, "\monn_{A, B}"'] & G(A \otimes B)  \mathrlap{,}
\end{tikzcd}
\]

for $A, B \in \catK$,

* an invertible 2-cell

\[
\begin{tikzcd}
F \unit
\ar[d, phantom, description, "\Two p^0"]
\ar[dr, "p_\unit"]   &
\\
\unit
\ar[ur, "\moni"]
\ar[rr, "\moni"']  &
\phantom{} &
G \unit \mathrlap{,}
\end{tikzcd}
\]

which satisfy the three coherence conditions  in <cit.>.

Let $p, q \co F \Rightarrow F'$ be monoidal pseudonatural transformations.
A monoidal modification from $p$ to $q$ is a modification $\phi \co p \Rrightarrow q$ which satisfies the two coherence conditions in <cit.>.

Note that the definition of a monoidal modification does not require additional structure on top of that of a modification.

The strictification theorem for monoidal bicategories, stated below for emphasis, follows as a scholium of the strictification theorem for tricategories [42, 45].

Every monoidal bicategory is biequivalent, as a monoidal bicategory, to a Gray monoid.

§.§ Symmetric monoidal bicategories and symmetric Gray monoids
We shall now recall the definition of a symmetric Gray monoid and of the relevant counterparts of lax monoidal pseudofunctors, monoidal transformations and monoidal modifications. For this, it is convenient to
arrive at symmetric Gray monoid by introducing progressively layers of structure and properties,
as in the notions of a braided and sylleptic Gray monoid, as illustrated in <ref>.

0-cells        1-cells     2-cells       3-cells
Gray monoid      Lax monoidal
pseudofunctors       Monoidal
transformations       Monoidal

Gray monoids       Braided lax monoidal
pseudofunctors       Braided monoidal

transformations       ”
Gray monoids     Sylleptic lax monoidal

pseudofunctors      ”      ”
Gray monoids       ”      ”      ”

Overview of Gray monoids.

The definitions of a braided Gray monoid in <ref> is equivalent to the one in <cit.>, but we state it in terms of the data considered in [10, 44, 41], <cit.>. This is a direct categorification of the notion of a braided monoidal category <cit.>, in that the two axioms for a braiding in the one-dimensional setting are replaced by two invertible modifications, written $\beta^1$ and $\beta^2$ below.

* A braided Gray monoid is a Gray monoid $\catK$ equipped with a pseudonatural equivalence with components on objects

\[
\bra_{A, B} \co A \otimes B \to B \otimes A \mathrlap{,}
\]

for $A, B \in \catK$, called the braiding, and invertible modifications with components

\begin{gather*}
\begin{tikzcd}[ampersand replacement=\&, column sep = small]
\&
B \otimes A \otimes C
\ar[d, phantom, description, "\Two \beta^1_{A,B,C}"]
\ar[dr, "\id_B \otimes \bra_{A,C}"]   \&
\\
A \otimes B \otimes C
\ar[ur, "\bra_{A, B} \otimes \id_C"]
\ar[rr, "\bra_{A, B \otimes C}"']  \&
\phantom{} \&
B \otimes C \otimes A \mathrlap{,}
\end{tikzcd} \\
\begin{tikzcd}[ampersand replacement=\&, column sep = small]
\&
A \otimes C \otimes B
\ar[d, phantom, description, "\Two \beta^2_{A, B, C}"]
\ar[dr, "\bra_{A, C} \otimes \id_B"]   \&
\\
A \otimes B \otimes C
\ar[ur, "\id_A \otimes \bra_{B, C}"]
\ar[rr, "\bra_{A \otimes B, C}"']  \&
\phantom{} \&
C \otimes A \otimes B  \mathrlap{,}
\end{tikzcd}
\end{gather*}

for $A, B \in \catK$, called the braiding constraints, such that

\[
\bra_{A, \unit} = \bra_{\unit, A} = \id_A
\]

for all $A \in \catK$, and which satisfy the coherence conditions in <cit.>, which include the four coherence
conditions in <cit.>.

* A sylleptic Gray monoid  is a braided Gray monoid $\catK$  equipped with an invertible modification with components

\[
\begin{tikzcd}
B \otimes A
\ar[d, phantom, description, "\Two \sigma_{A, B}"]
\ar[dr, "\bra_{B, A}"]   &
\\
A \otimes B
\ar[rr, "\id_{A \otimes B}"']
\ar[ur, "\bra_{A, B}"]  &
\phantom{} &
A \otimes B  \mathrlap{,}
\end{tikzcd}
\]

for $A, B \in \catK$, called the syllepsis, which satisfies the two coherence conditions in <cit.>.

* A symmetric Gray monoid is a sylleptic Gray monoid such that the syllepsis $\sigma$ satisfies the additional condition for it to be a symmetry <cit.>.

Next, we consider the counterparts of lax monoidal pseudofunctors for braided and sylleptic Gray monoids.

* Let $\catK$ and $\catL$ be braided Gray monoids. A  braided lax monoidal pseudofunctor from $\catK$ to $\catL$ is a lax monoidal pseudofunctor
$F  \co \catK \to \catL$ equipped with
an invertible modification with components on objects

\[
\begin{tikzcd}[column sep = large]
FA \otimes FB \ar[r, "\bra_{A,B}"] \ar[d, "\monn_{A, B}"'] \ar[dr,phantom,"\Two"]   & FB \otimes FA \ar[d, "\monn_{B,A}"] \\
F(A \otimes B) \ar[r, "F(\bra_{A, B})"'] & F(B \otimes A) \mathrlap{,}
\end{tikzcd}
\]

for $A, B \in \catK$, which satisfies the two axioms in <cit.>.

* Let $\catK$ and $\catL$ be sylleptic Gray monoids. A sylleptic lax monoidal pseudofunctor from $\catK$ to $\catL$ is a braided lax monoidal pseudofunctor
$F  \co \catK \to \catL$ which satisfies the additional axiom in <cit.> or <cit.>.

Note that the appropriate morphisms between symmetric  Gray monoids are sylleptic lax monoidal pseudofunctors, since a symmetric Gray monoid is merely a sylleptic Gray monoid which satisfies an additional property,  <cit.>.

Let $F, G \co \catK \to \catL$ be braided lax monoidal pseudofunctors. A braided monoidal pseudonatural transformation from $F$ to $G$
is a monoidal pseudonatural transformation $p \co F \Rightarrow G$ which satisfies the additional coherence condition in  <cit.>.

Analogously to what we said above for pseudofunctors, the appropriate morphisms between
sylleptic lax monoidal pseudofunctors are braided monoidal pseudonatural transformations
since a sylleptic lax monoidal pseudofunctor is merely a  braided lax monoidal pseudofunctor satisfying an additional property. And since these are just monoidal transformations which satisfy an additional
property, the appropriate morphisms between them are the monoidal modifications of <ref>.

The next strictification result is recalled from <cit.>.

Every symmetric monoidal bicategory is equivalent, as a symmetric monoidal bicategory, to a symmetric  Gray monoid.

Without loss of generality it is possible to assume that the additional equations for a strict symmetric monoidal 2-category, in the sense of <cit.>, hold as well.
These include those for a braided monoidal 2-category in the sense of <cit.>. In the following, we will use <ref> and <ref> and  the associated principles of transport of structure to limit ourselves to consider (symmetric) Gray monoids. Provided
that the structure and properties under consideration are invariant under (symmetric) monoidal biequivalence, one obtains results on (symmetric) monoidal bicategories (remarks at the
start of <ref>).

In the following, we shall frequently refer to coherence conditions. We will do so using
the order in which they appear in the reference provided in the definition given here. For example,
the first coherence axiom for a lax monoidal pseudofunctor (<ref>) means the first
coherence axiom in <cit.>, which involves an
equality between a pasting diagram
involving $\omega$ and $\zeta$ and a pasting diagram involving $\kappa$.

§ PSEUDOCOMONOIDS AND PSEUDOBIALGEBRAS

§.§ Pseudocomonoids

In preparation for the material on linear exponential pseudocomonads in <ref>, we recall some basic material on pseudocomonoids from [23] and prove some auxiliary results about them, which we could not find in the existing literature and may be of independent interest.
The definitions of a  pseudocomonoid, braided pseudocomonoid and symmetric pseudocomonoid are analogous to those of monoidal category, braided monoidal category and symmetric monoidal category, respectively.
Accordingly, the definitions of a pseudocomonoid morphism and of a braided pseudocomonoid morphism are analogous to those of strong monoidal functor and braided monoidal functor. Finally, pseudocomonoid 2-cells are
counterparts of monoidal transformations.
In particular, the same pattern of distinction between structure and property arises, <ref>.

Let $\catK$ be a Gray monoid.

A pseudocomonoid in $\catK$ is an object $A \in \catK$ equipped with

* a map $n \co A \to A \otimes A$, called the comultiplication,

* a map $e \co A \to  \unit$, called counit,

* invertible 2-cells

\begin{equation*}
\begin{tikzcd}[column sep = large]
A \ar[r, "n"] \ar[d, "n"']  \ar[dr,phantom,"\Two \alpha"] & A \otimes A \ar[d, "n \otimes \id_A "] \\
A \otimes A \ar[r, "\id_A \otimes n"'] & A \otimes A \otimes A  \mathrlap{,}
\end{tikzcd}
\end{equation*}

called the associativity constraint, and

\begin{equation*}
\begin{tikzcd}[column sep = {1.5cm,between origins}]
A \otimes A
\ar[d, phantom, description, "\Two \lambda"]
\ar[dr, "e \otimes \id_A"]   &
\\
\ar[ur, "n"]
\ar[rr, "\id_A"']  &
\phantom{} &
A \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}[column sep = {1.5cm,between origins}]
A \otimes A
\ar[d, phantom, description, "\Two \rho"]
\ar[dr, "\id_A \otimes e"]   &
\\
\ar[ur, "n"]
\ar[rr, "\id_A"']  &
\phantom{} &
A  \mathrlap{,}
\end{tikzcd}
\end{equation*}

called the left and right unitality constraints, respectively,

which satisfy the duals of the two coherence conditions in <cit.>. (These are analogous to those for a monoidal category.)

In the following, we use the letters $n$ and $e$ to denote the comultiplication and counit of different pseudocomonoids when this does not cause confusion.

Let $A$ and $B$ be pseudocomonoids in $\catK$. A  pseudocomonoid morphism from $A$ to $B$ is a
map $f \co A \to B$ equipped with

* an invertible 2-cell

\[
\begin{tikzcd}
A \ar[r, "f"] \ar[d, "\com"']  \ar[dr,phantom,"\Two \bar{f}"] & B \ar[d, "\com"]  \\
A \otimes A \ar[r, "f \otimes f"'] & B \otimes B \mathrlap{,}
\end{tikzcd}
\]

* an invertible 2-cell

\[
\begin{tikzcd}
A \ar[d, "\cou"'] \ar[r, "f"]    \ar[dr,phantom,"\Two \tilde{f}"] & B \ar[d, "\cou"] \\
\unit \ar[r, "\id_\unit"'] &  \unit \mathrlap{,}
\end{tikzcd}
\]

which satisfy three coherence conditions. (These are analogous to those for a lax monoidal functor <cit.>.)

Let $f, g \co A \to B$ be  pseudocomonoid morphisms in $\catK$. A pseudocomonoid $2$-cell from $f$ to $g$
is a 2-cell $\alpha \co f \Rightarrow g$ which satisfies two coherence conditions. (These are analogous to those for a monoidal natural
transformation <cit.>.)

We write $\CoMon{\catK}$ for the 2-category of pseudocomonoids, pseudocomonoid morphisms, and pseudocomonoid 2-cells in $\catK$.
Let us now assume that  $\catK$ is braided.

A braided pseudocomonoid is a pseudocomonoid $A$ equipped with an invertible 2-cell

\begin{equation}
\label{equ:braiding-comonoid}
\begin{tikzcd}[column sep = {1.5cm,between origins}]
A \otimes A
\ar[d, phantom, description, "\Two \gamma"]
\ar[dr, "\bra_{A,A}"]   &
\\
\ar[ur, "\com"]
\ar[rr, "\com"']  &
\phantom{} &
A \otimes A
\end{tikzcd}
\end{equation}

which satisfies the duals of the two coherence conditions in <cit.>. (These are analogous to those for a braided monoidal category <cit.>.)

Let $A$ and $B$ be braided pseudocomonoids in $\catK$. A braided pseudocomonoid morphism from $A$ to $B$ is a
pseudocomoid morphism  $f \co A \to B$ which satisfies one additional coherence condition. (This is analogous to that for a lax monoidal functor to be braided <cit.>.)

We write $\BraCoMon{\catK}$ for the 2-category of braided pseudocomonoids, braided pseudocomonoid morphisms, and pseudocomonoid 2-cells  in $\catK$.
Let us now assume that $\catK$ is sylleptic.

A symmetric pseudocomonoid in $\catK$ is a braided pseudocomonoid in $\catK$ whose braiding satisfies
the additional coherence condition for a symmetry <cit.>. (This is analogous to the axiom for a braided monoidal category to be symmetric.)

We write $\SymCoMon{\catK}$ for the 2-category of symmetric pseudocomonoids, braided pseudocomonoid morphisms, and pseudocomonoid 2-cells in $\catK$.
The definitions of the 2-categories $\CoMon{\catK}$, $\BraCoMon{\catK}$, and $\SymCoMon{\catK}$ is summarised in <ref>.
There are evident duals of these notions, giving rise to the 2-categories $\Mon{\catK}$, $\BraMon{\catK}$, and $\SymMon{\catK}$ of
pseudomonoids, braided pseudomonoids and symmetric pseudomonoids, respectively, in $\catK$.

0-cells      1-cells        2-cells
$\CoMon{\catK}$      Pseudocomonoids       Pseudocomonoid
morphisms      Pseudocomonoid
$\BraCoMon{\catK}$      Braided
pseudocomonoids      Braided
pseudocomonoid morphisms      ”
$\SymCoMon{\catK}$         Symmetric
pseudocomonoid     ”     ”

Overview of pseudocomonoids.

<ref> below recalls from <cit.> the two-dimensional counterpart of the well-known one-dimensional result asserting that the category of commutative comonoids in a symmetric monoidal category has finite products. Recall from <ref> that we mean finite products in a bicategorical sense.

Let $\catK$ be a symmetric Gray monoid. The 2-category $\SymCoMon{\catK}$ of symmetric pseudocomonoids in $\catK$ has finite products.

We outline the definition of the binary products and of terminal object of $\SymCoMon{\catK}$. We begin by recalling that if $A$ and $B$ are symmetric pseudocomonoids  in $\catK$, the tensor product of their
underlying objects $A \otimes B$ in $\catK$ admits the structure of a symmetric pseudocomonoid. Indeed, the tensor product in a symmetric Gray monoid $\catK$ is a sylleptic strong monoidal pseudofunctor <cit.>,
and therefore it preserves symmetric pseudocomonoids <cit.>. Thus, it lifts as follows:

\begin{equation*}
\begin{tikzcd}[column sep = large]
\SymCoMon{\catK} \times \CoMon{\catK} \ar[r, "(-) \otimes (=)"] \ar[d, "U \times U"'] &
\SymCoMon{\catK} \ar[d, "U"] \\
\catK \times \catK \ar[r, "(-) \otimes (=)"']  &
\catK \mathrlap{.}
\end{tikzcd}
\end{equation*}

Explicitly, the comultiplication and counit are the following composites:

\begin{gather}
\label{equ:comultiplication-for-tensor}
\begin{tikzcd}[ampersand replacement=\&]
A \otimes B
\ar[r, "\com \otimes \com"] \&
A \otimes A \otimes B \otimes B
\ar[r, "\id_A \otimes \bra_{A,B} \otimes \id_A"] \&[4em]
A \otimes B \otimes A \otimes B  \mathrlap{,}
\end{tikzcd} \\
\label{equ:counit-for-tensor}
\begin{tikzcd}[ampersand replacement=\&]
A \otimes B
\ar[r, "e \otimes e"] \&
\unit \otimes \unit
\ar[r, "\id"] \&
\unit \mathrlap{.}
\end{tikzcd}
\end{gather}

The associativity constraint is

\[
\begin{tikzcd}[scale=0.75]
A \otimes B \ar[r, "\com \otimes \com"] \ar[d, "\com \otimes \com"']  \ar[dr,phantom,"\Two \alpha \otimes \alpha"]  &[3em]
A \otimes A \otimes B \otimes B \ar[r, "\id_A \otimes \bra_{A,B} \otimes \id_B"] \ar[d, "\com \otimes \id_A \otimes \com \otimes \id_B"] \ar[dr,phantom,"\cong"]  &[6em]
A \otimes B \otimes A \otimes B \ar[d, "\com \otimes \com \otimes \id_A \otimes \id_B"] \\
A \otimes A \otimes B \otimes B \ar[r, "\id_A \otimes \com \otimes \id_B  \otimes \com"']  \ar[d, "\id_A \otimes \bra_{A,B} \otimes \id_B"']  \ar[dr,phantom,"\cong"] &
A \otimes A \otimes A \otimes B \otimes B \otimes B  \ar[r, "\id_A \otimes \id_A \otimes \bra_{A,B \otimes B} \otimes \id_B"]  \ar[d, "\id \otimes \bra_{A \otimes A,B} \otimes \id_B \otimes \id_B"]  \ar[dr,phantom,"\Two \id_A \otimes \xi \otimes \id_B"]  &
A \otimes A \otimes B \otimes B \otimes A \otimes B \ar[d, "\id_A \otimes \bra_{A,B} \otimes \id_B \otimes \id_A \otimes \id_B"] \\
A \otimes B \otimes A \otimes B \ar[r, "\id_A \otimes \id_B \otimes \com \otimes \com"']  &
A \otimes B \times A \otimes A \otimes B \otimes B  \ar[r, "\id_A \otimes \id_B \otimes \id_A \otimes \bra_{A,B} \otimes \id_B"']   &
A \otimes B \times A \otimes B \otimes A \otimes B \mathrlap{,}
\end{tikzcd}
\]

where $\xi$ is an invertible 2-cell which can easily be constructed using the two braiding constraints $\beta_1$ and $\beta_2$ of <ref>.

The left unitality constraint is

\[
\begin{tikzcd}
A \otimes B
\ar[r, "\com \otimes \com"]
\ar[dr, bend right = 20, "\id"'] &
A \otimes A \otimes B \otimes B
\ar[r, "\id \otimes \bra_{A, B} \otimes \id"]
\ar[d, "e \otimes \id \otimes e \otimes \id"] \ar[dr,phantom,"\cong"] &[5em]
A \otimes B \otimes A \otimes B
\ar[d, "e \otimes e \otimes \id \otimes \id"] \\
\phantom{} \ar[ur, phantom, description, pos=(.6), "\Two \lambda \otimes \lambda"]
& \unit \otimes A \otimes \unit \otimes B \ar[r, "\id \otimes \bra_{A, \unit} \otimes \id"'] & \unit \otimes \unit \otimes A \otimes B \mathrlap{.}
\end{tikzcd}
\]

The right unitality constraint is

\[
\begin{tikzcd}
A \otimes B \ar[r, "\com \otimes \com"] \ar[dr,  bend right = 20,  "\id"']  & A \otimes A \otimes B \otimes B \ar[r, "\id \otimes \bra_{A,B} \otimes \id"] \ar[d, "\id \otimes e \otimes \id \otimes e"] \ar[dr,phantom,"\cong"]  &[5em] A \otimes B \otimes A \otimes B \ar[d, "\id \otimes \id \otimes e \otimes e"]  \\
\phantom{} \ar[ur, phantom, description, pos=(.6), "\Two \rho \otimes \rho"]
&  A \otimes \unit \otimes B \otimes \unit  \ar[r, "\id \otimes \bra_{\unit, B} \otimes \id"']  & \otimes A \otimes B \otimes \unit \otimes \unit \mathrlap{.}
\end{tikzcd}
\]

The symmetry is a 2-cell of the form

\[
\begin{tikzcd}
A \otimes B
\ar[r, "\com \otimes \com"]
\ar[dr,  bend right = 20,  "\com \otimes \com"'] &[3em]
A \otimes A \otimes B \otimes B
\ar[r, "\id_A \otimes \bra_{A,B} \otimes \id_B"]
\ar[d,  "\bra_{A,A} \otimes \bra_{B,B}"] \ar[dr,phantom,"\Two \sigma'"]  &[7em]
A \otimes B \otimes A \otimes B
\ar[d, "\bra_{A \otimes B, A\otimes B}"]  \\
\phantom{} \ar[ur, phantom, description, pos=(.6), "\Two \gamma \otimes \gamma"]  &
A \otimes A \otimes B \otimes B
\ar[r, "\id_A \otimes \bra_{A,B} \otimes \id_B"'] &
A \otimes B \otimes A \otimes B
\end{tikzcd}
\]

where $\sigma'$ is an invertible 2-cell constructed using the braiding constraints $\beta^1$, $\beta^2$ and the symmetry $\sigma$ of $\catK$.

It is then possible to show that $A \otimes B$ is the product of $A$ and $B$ in $\SymCoMon{\catK}$, when considered equipped with the projections $\pi_1 \co A \otimes B \to A$ and $\pi_2 \co A \otimes B \to B$  given by
the following composites:

\[
\begin{tikzcd}
A \otimes B \ar[r, "\id_A \otimes e"] &
A \otimes \unit \ar[r, "\id"] &
A \mathrlap{,}
\end{tikzcd} \quad
\begin{tikzcd}
A \otimes B \ar[r, "e \otimes \id_B"] &
\unit \otimes B \ar[r, "\id"] &
B \mathrlap{,}
\end{tikzcd}
\]

respectively, both of which can be shown to be braided pseudocomonoid morphisms.

The terminal object of $\SymCoMon{\catK}$ is the unit $\unit$ of $\catK$, viewed as a symmetric pseudocomonoid in the evident way. For a symmetric pseudomonoid $A$, the required essentially unique braided pseudocomonoid morphism to $\unit$ is the counit of $A$.

Let $\catK$ be a symmetric Gray monoid. The 2-category $\SymCoMon{\catK}$ of symmetric pseudocomonoids in $\catK$ admits a symmetric monoidal structure such that the forgetful 2-functor

\[
U \co \SymCoMon{\catK} \to \catK
\]

is  strict symmetric monoidal.

Combine <ref> with <cit.>.

Of course, <ref> could also be established directly (without appealing to <ref>), but we prefer to not to do so for brevity. One of the reasons for our interest in <ref> is that it
allows us to introduce the notion of a symmetric pseudobialgebra in a concise way,
as done in <ref>, just as it can be done for commutative bialgebras in the one-dimensional setting [2].
The definition is restated in an equivalent way and unfolded explicitly in <ref>.

A symmetric pseudobialgebra in $\catK$ is a symmetric pseudomonoid in $\SymCoMon{\catK}$.

In analogy with the one-dimensional situation, a symmetric pseudobialgebra can be defined equivalently as a symmetric pseudocomonoid in the 2-category $\SymMon{\catK}$ of symmetric pseudomonoids, braided pseudomonoid morphisms and pseudomonoid 2-cells. Indeed, assume that we have

* an object $A \in \catK$,

* maps $\com \co A \to A \otimes A$, $e \co A \to I$ in $\catK$, and invertible 2-cells $\alpha$, $\lambda$, $\rho$ and $\gamma$ equipping $A$ with the structure of a braided pseudocomonoid in $\catK$,
as in <ref> and <ref>,

* maps $m \co A \otimes A \to A$ and $u \co I \to A$ in $\catK$ and invertible 2-cells

\[
\begin{tikzcd}[column sep = large]
A \otimes A  \otimes A \ar[r, "\id_A \otimes m "] \ar[d, " m \otimes \id_A"']  \ar[dr,phantom,"\Two \beta"] & A \otimes A \ar[d, "m  "] \\
A \otimes A \ar[r, " m"'] & A   \mathrlap{,}
\end{tikzcd}
\]

\[
\begin{tikzcd}[column sep = {1.5cm,between origins}]
\ar[d, phantom, description, "\Two \sigma"]
\ar[dr, "m"]   &
\\
A \otimes A
\ar[ur, "u \otimes \id_A"]
\ar[rr, "\id_A"']  &
\phantom{} &
A  \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}[column sep = {1.5cm,between origins}]
\ar[d, phantom, description, "\Two \tau"]
\ar[dr, "m"]   &
\\
A \otimes A
\ar[ur, "\id_A \otimes u"]
\ar[rr, "\id_A"']  &
\phantom{} &
A \otimes A \mathrlap{,}
\end{tikzcd}
\]

\[
\begin{tikzcd}[column sep = {1.5cm,between origins}]
A \otimes A
\ar[d, phantom, description, "\Two \delta"]
\ar[dr, "m"]   &
\\
\ar[ur, "\bra_{A,A}"]
\ar[rr, "m"']  &
\phantom{} &
A \otimes A
\end{tikzcd}
\]

equipping $A$ with the structure of a braided pseudomonoid in $\catK$.

Then, there is a bijection between:

* the set of 4-tuples of invertible 2-cells making $m \co A \otimes A \to A$ and $u \co I \to A$ into braided pseucodomonoid morphisms such that $\beta$, $\sigma$, $\tau$ and $\delta$ are pseudocomonoid 2-cells,
which therefore determine a symmetric pseudomonoid in $\SymCoMon{\catK}$;

* the set of 4-tuples of invertible 2-cells making $\com \co A \to A \otimes A$ and $e \co A \to I$ into  braided pseudomonoid morphisms such that $\alpha$, $\lambda$, $\rho$ and $\gamma$ are pseudomonoid 2-cells,
which therefore determine a symmetric pseudocomonoid in $\SymMon{\catK}$.

In this correspondence, the coherence conditions for the braided pseudomonoid morphisms and for pseudocomonoid 2-cells in (i) imply the coherence conditions for the pseudocomonoid 2-cells and
for the braided pseudomonoid morphisms in (ii), respectively.

Since <ref> is stated in terms of the data in (i), let us record for reference that the 2-cells therein have the form

\[
\begin{tikzcd}[column sep = large]
A \otimes A
\ar[r, "m"]
\ar[d, "\com \otimes \com"']
\ar[ddr, phantom, description, "\Two \bar{m}"] &
A \ar[dd, "\com"]  \\
A \otimes A \otimes A \otimes A
\ar[d, "\id_A \otimes \bra_{A,A} \otimes \id_A"']
& \\
A \otimes A \otimes A \otimes A \ar[r, "m \otimes m"'] &
A \otimes A \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}
A \otimes A
\ar[r, "m"]
\ar[dd, "e \otimes e"']
\ar[ddr, phantom, description, "\Two \tilde{m}"] &
A  \ar[dd, "\cou"]  \\
& \\
\unit \otimes \unit \ar[r, "\id"'] &
\unit \mathrlap{,}
\end{tikzcd}
\]

\[
\qquad
\begin{tikzcd}
\unit
\ar[r, "u"]
\ar[d, "\id"']
\ar[dr, phantom, description, "\Two \tilde{u}"] &[4em]
\ar[d, "\com"] \\
\unit
\ar[r, "u \otimes u"']  &
A \otimes A \mathrlap{,}
\end{tikzcd}  \qquad
\begin{tikzcd}
\unit \otimes \unit
\ar[d, "\id"']
\ar[r, "u"]
\ar[dr, phantom, description, "\Two \bar{u}"] &
A \ar[d, "\cou"] \\
\unit
\ar[r, "\id"']  &
\unit
\mathrlap{.}
\end{tikzcd} \qquad
\]

§.§ Products, coproducts and biproducts

We recall and establish some facts regarding cartesian and cocartesian monoidal structures. Recall from <ref> our conventions and notation regarding products and coproducts in a 2-category.

Let $\catK$ be a symmetric Gray monoid.
The monoidal structure of $\catK$ is cartesian if and only if every $A \in \catK$ admits a symmetric pseudocomonoid structure in $\catK$, pseudonaturally and monoidally in $A$.

For one implication, assume that $\catK$ is cartesian. It is immediate to check that $A \in \catK$ admits a symmetric pseudocomonoid structure with comultiplication the
diagonal $\Delta_A \co A \to A \with A$ and counit the essentially unique map $A \to \term$.  For the converse implication, the hypotheses amount to saying that we have not only a biequivalence

\[
\begin{tikzcd}[column sep = large]
\catK
\ar[r, shift left =2, "F"]
\ar[r, description, phantom, "\scriptstyle \simeq"] &
\SymCoMon{\catK} \mathrlap{,}
\ar[l, shift left =2, "U"]
\end{tikzcd}
\]

where $F$ assigns to $A$ the canonical symmetric pseudomonoid on it and $U$ is the forgetful functor, but that this is a symmetric monoidal biequivalence, where $\catK$ is considered
with its symmetric Gray monoid structure and $\SymCoMon{\catK}$ is considered with the symmetric monoidal structure of <ref>.
The claim now follows from <ref>.

For the next lemma, recall what we mean by preservation of finite products from the start of <ref>.

Let $\catK$ and $\catL$ be 2-categories with finite products and $F \co \catK \to \catL$ be a 2-functor that preserves finite products.
Then for every $A \in \catK$, the following
symmetric pseudocomonoids in $\catL$ are equivalent as symmetric pseudocomonoids:

* the symmetric pseudomonoid on $FA$ obtained by applying $F$ to the canonical pseudocomonoid on $A$ determined by finite products in $\catK$, with comultiplication and counit

\[
\begin{tikzcd}
FA \ar[r, "F(\Delta_A)"] &[2em]  F(A \with A) \ar[r, "\simeq"] &  FA \with FA  \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}
FA \ar[r, "F(\textup{can})"]  &[2em] F(\term) \ar[r, "\sim"] & \term \mathrlap{,}
\end{tikzcd}
\]

* the symmetric pseudocomonod on $FA$ determined by finite products in $\catL$, with comultiplication and counit

\[
\begin{tikzcd}
FA \ar[r, "\Delta_{FA}"] &[1em] FA \with FA  \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}
FA \ar[r, "\textup{can}"]  &[1em]  \term \mathrlap{.}
\end{tikzcd}
\]

Direct calculation.

We conclude this section with our definition of a biproduct and a basic fact about it, which will be useful for  <ref>.

Let $\catK$ be a 2-category with finite products and finite coproducts. We say that $\catK$ has biproducts if there are equivalences
$A + B \to A \with B$, for all $A, B \in \catK$, and $0 \to \term$.

If a 2-category $\catK$ has biproducts, we identify product and coproducts, call them biproducts, and write $A \oplus B$ for the biproduct of $A$ and $B$. We also identify the initial and terminal object, write $0$ for it and call it the zero object of $\catK$. The next result builds on <ref>.

Let $\catK$ be a 2-category with biproducts. For every object $A \in \catK$, the symmetric pseudomonoid structure on $A$ determined by  products,

\[
\Delta_A \co A \to A \oplus A \mathrlap{,} \quad A \to 0  \mathrlap{,}
\]

and the symmetric pseudocomonoid structure on $A$, determined by coproducts,

\[
\nabla_A \co A \oplus A \to A \mathrlap{,} \quad 0 \to A \mathrlap{,}
\]

determine a symmetric pseudobialgebra structure on $A$.

The symmetric monoidal structure determined by biproducts is both cartesian and cocartesian and therefore every object $A \in \catK$ has both the structure of a  symmetric pseudocomonoid
and of a  symmetric pseudomonoid by <ref> and its dual. It remains to check that the multiplication (the codiagonal $\nabla_A \co A \oplus A \to A$) and the counit (the essentially unique map $A \to 0$) are braided pseudocomonoid morphisms and that the associativity and unitality constraints are pseudocomonoid 2-cells, but this is true for any map and any 2-cell in a cocartesian monoidal structure.

§ LINEAR EXPONENTIAL PSEUDOCOMONADS

The goal of this section is to introduce our bicategorical counterpart of the notion of a linear exponential comonad and prove some basic facts about it. Our formulation is based on the
definition of linear exponential comonad in [47]. We compare our notion with the one in [50] in <ref> below.

§.§ Pseudocomonads

As a first step, we recall the definition of a pseudocomonad, which is dual to that of a pseudomonad [61].
We consider pseudocomonads whose underlying pseudofunctor is a 2-functor, as justified by the
strictification theorems in [13, 61],  <cit.>.

Let $\catK$ be a 2-category.  A pseudocomonad on $\catK$ is a 2-functor $\bang(-) \co \catK \to \catK$ equipped with:

* a pseudonatural transformation with components on objects $\dig_A \co \bang A \to \bbang A$, for $A \in \catK$, called the comultiplication of the pseudocomonad,

* a pseudonatural transformation with components on objects  $\der_A \co \bang A \to A$, for $A \in \catK$, called the counit of the pseudocomonad,

* an invertible modifications with components

\[
\begin{tikzcd}[column sep = large]
\bang A \ar[r, "\dig_A"] \ar[d, "\dig_A"']  \ar[dr,phantom,"\Two \pi_A"] & \bbang A \ar[d, "\bang \dig_A"] \\
\bbang A \ar[r, "\dig_{\bang A} "'] & \bbbang A  \mathrlap{,}
\end{tikzcd}
\]

for $A \in \catK$, called the associativity constraint of the pseudocomonad,

* two invertible modifcations

\[
\begin{tikzcd}[column sep = {1.5cm,between origins}]
\bbang A
\ar[d, phantom, description, "\Two \mu_A"]
\ar[dr, "\der_{\bang A}"]   &
\\
\bang A
\ar[ur, "\dig_A"]
\ar[rr, "\id_{\bang A}"']  &
\phantom{} &
\bang A \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}[column sep = {1.5cm,between origins}]
\bbang A
\ar[d, phantom, description, "\Two \nu_A"]
\ar[dr, "\bang \der_A"]   &
\\
\bang A
\ar[ur, "\dig_A"]
\ar[rr, "\id_{\bang A}"']  &
\phantom{} &
\bang A \mathrlap{,}
\end{tikzcd}
\end{equation*}
for $A \in \catK$, called the  (left and right) \emph{unitality constraints} of the pseudocomonad,
\end{itemize}
which satisfy two coherence conditions. (These are dual to those for a pseudomonad~\cite[Section~1]{LackS:cohap}.)
\end{definition}

The notation for a pseudocomonad adopted here\footnote{The slightly unorthodox choice of the Greek letters $\pi$, $\mu$, $\nu$ for the pseudocomonad
constraints is intended to avoid a clash with the notation for the constraints of a pseudomonoid, \cf \cref{thm:comonoid}. This is especially useful in view of the formulation of a linear exponential pseudocomonad
in \cref{thm:linear-exponential-comonad}, which will involve both notions.} is inspired by the literature on
categorical models of Linear Logic, where the underlying 2-functor of the pseudocomonad corresponds to the exponential modality,
the comultiplication to the promotion rule, and the comultiplication to the dereliction rule~[64].

Let us now fix a 2-category $\catK$ and a pseudocomonad $(\bang, \dig, \der)$ on it as in \cref{def:psd-comonad}.

\begin{definition} An \emph{pseudocoalgebra} for the pseudocomonad is an object $A \in \catK$ equipped with:
\begin{itemize}
\item a map $a \co A \to \bang A$, called the \emph{structure map} of the pseudocoalgebra,
\item two invertible 2-cells
\[
\begin{tikzcd}[column sep = large]
A \ar[r, "a"] \ar[d, "a"'] \ar[dr,phantom,"\Two \bar{a}"] & \bang A \ar[d, "\dig_A"] \\
\bang A \ar[r, "\bang a"'] &  \bbang A \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}[column sep = large]
A \ar[r, "a"] \ar[dr, bend right = 20,  "\id_A"'] & \bang A \ar[d, "\der_A"] \\
\phantom{} \ar[ur, phantom, {pos=.7},  "\Two \tilde{a}"] & A \mathrlap{,}
\end{tikzcd}
\]
called the \emph{associativity} and \emph{unitality} constraints of the pseudocoalgebra,
\end{itemize}
which satisfy  two coherence conditions. (These are dual to those for a pseudoalgebra~\cite[Section~4.2]{LackS:cohap}.)
\end{definition}

\begin{definition} Let $A$ and $B$ be pseudocoalgebras in $\catK$. A \myemph{pseudocoalgebra morphism} from $A$ to $B$ is
a map $f \co A \to B$ equipped with an invertible 2-cell
\[
\begin{tikzcd}
A \ar[r, "f"] \ar[d, "a"'] \ar[dr,phantom,"\Two \bar{f}"] & B \ar[d, "b"] \\
\bang A \ar[r, "\bang f"'] & \bang B
\end{tikzcd}
\]
which satisfy  two coherence conditions. (These are dual to those for a pseudoalgebra morphism~\cite[Section~1.2]{BlackwellR:twodmt}.)
\end{definition}

\begin{definition} Let $f, g \co A \to B$ be pseudocoalgebra morphisms in $\catK$. A \myemph{coalgebra $2$-cell} from $f$ to $g$ is a
2-cell $\phi \co f \Rightarrow g$ which satisfies one coherence condition. (This is dual to that for a pseudoalgebra 2-cell~\cite[Section~1.2]{BlackwellR:twodmt}.)
\end{definition}

We write $\Em{\catK}$ for the 2-category of  pseudocoalgebras, pseudocoalgebra morphisms and pseudocoalgebra 2-cells. This is connected to $\catK$ by
a biadjunction
\begin{equation}
\label{equ:em-adjunction}
\begin{tikzcd}[column sep = large]
\catK
\ar[r, shift right =1, bend right = 10, "F"']
\ar[r, description, phantom, "\scriptstyle \bot"] &
\Em{\catK}   \mathrlap{,}
\ar[l, shift right = 1, bend right = 10, "U"']
\end{tikzcd}
\end{equation}
where the left biadjoint $U$ is the evident forgetful 2-functor, sending a pseudocoalgebra to its underlying object, and the right biadjoint $F$ sends
an object $B \in \catK$ to the cofree pseudocoalgebra on $B$, given by $\bang B$, viewed as a pseudocoalgebra with structure map
$\dig_B \co \bang B \to \bbang B$. The associativity and unit constraints of the pseudocoalgebra  are obtained from those of the pseudocomonad.

In view of application in \cref{sec:products}, let us unfold more explicitly the biadjunction in~\eqref{equ:em-adjunction} in terms of universal properties.
For $B \in \catK$, the universal property of the pseudocoalgebra $\bang B$ means that for every pseudocoalgebra~$A$, with structure map $a \co A \to \bang A$,
composition with $\der_B \co \bang B \to B$  gives an adjoint equivalence of categories
\begin{equation}
\label{equ:aux-equiv}
\begin{tikzcd}[column sep = large]
\Em{\catK}[ A, \bang B]   \ar[r, "(-) \der_B"] &
\catK[A, B]  \mathrlap{.}
\end{tikzcd}
\end{equation}
In particular, for every $f \co A \to B$ in $\catK$, there is an essentially unique  pseudocoalgebra morphism $f^\sharp \co A \to \bang B$  such that $\der_B \circ f^\sharp \cong f$ in $\catK$. Here, essential
uniqueness refers to the fact that \eqref{equ:aux-equiv} is an equivalence, rather than an isomorphism.
Explicitly, $f^\sharp \co A \to \bang B$ is obtained as the composite
\begin{equation}
\label{equ:unfold-f-sharp}
\begin{tikzcd}
A \ar[r, "a"] &
\bang A \ar[r, "\bang f"] &
\bang B \mathrlap{.}
\end{tikzcd}
\end{equation}

We shall also make use of the Kleisli bicategory of the pseudocomonad, written $\Kl{\catK}$, whose objects
are the objects of~$\catK$ and whose hom-categories are defined by letting $\Kl{\catK}[A, B] \defeq \catK[\bang A, B]$,
for $A, B \in \catK$. As observed in~[15], in general $\Kl{\catK}$ is a  bicategory, not a 2-category. There is a biadjunction
\begin{equation}
\label{equ:cokleisliadjunction}
\begin{tikzcd}[column sep = large]
\Kl{\catK}
\ar[r, shift left =1, bend left =10, "K"]
\ar[r, description, phantom, "\scriptstyle \bot"] &
\catK \mathrlap{.}
\ar[l, shift left = 1, bend left =10, "J"]
\end{tikzcd}
\end{equation}
The left biadjoint $K$ sends $A \in \Kl{\catK} $ to $\bang A \in \catK$ and $f  \co \bang A \to B$ to the composite $\bang f \circ \dig_A \co \bang A \to \bang B$, while the right biadjoint $J$ is the identity on objects and sends a map $f \co A \to B$ to the composite $f \circ \der_A \co \bang A \to B$.

It is immediate to check that if $\catK$ has finite products, so does $\Kl \catK$. We record this as a proposition as we will use it in the proof of \cref{thm:coKleisli-cartesian-closed}.

\begin{proposition} \label{thm:coKleisli-cartesian}
Let $\catK$ be 2-category  and $(\bang, \dig, \der)$ a pseudocomonad on it. Assume $\catK$ has finite products.
Then the  Kleisli bicategory $\Kl \catK$ has finite products.
\end{proposition}

\begin{proof} We define the product of  $A$ and $B$ in $\Kl \catK$ to be their product $A \with B$ in $\catK$.
The required universal property follows from the equivalence
\begin{align*}
\Kl \catK [ X, A] \times \Kl \catK  [X, B]  & = \catK[ \bang X, A] \times \catK[\bang X, B] \\
& \simeq \catK[ \bang X, A \with B] \\
& = \Kl \catK  [ X, A \with B] \mathrlap{,}
\end{align*}
for every $X, A, B \in \catK$.
The terminal object $\Kl \catK $ is the terminal object of $\catK$. Indeed, we have the equivalence
\[
\Kl \catK [ A, \term]  =
\catK[\bang A, \term] \simeq
\mathsf{1} \mathrlap{,}
\]
for every $A \in \catK$.
\end{proof}

\subsection*{Symmetric lax monoidal pseudocomonads} As a second step towards our notion of a linear exponential pseudocomonad, we give the definition of a
symmetric lax monoidal pseudocomonad, assuming that $\catK$ has the structure of a symmetric Gray monoid. The definition involves not only
the underlying 2-functor, comultiplication and counit interacting suitably with the symmetric monoidal structure, but also the additional modifications
for associativity and unit laws.

\begin{definition} \label{thm:sym-lax-monoidal-pseudocomonad}
Let $\catK$ be a symmetric Gray monoid. A \myemph{symmetric lax monoidal pseudocomonad} on $\catK$ is  a pseudocomonad
$(\bang, \dig, \der)$ on $\catK$ as in \cref{def:psd-comonad} equipped with additional structure and satisfying extra properties as follows:
\begin{itemize}
\item the underlying 2-functor of the pseudocomonad is sylleptic lax monoidal, \ie we have a pseudonatural transformations with object components
\begin{equation}
\label{equ:monn}
\monn_{A, B} \co \bang A \otimes \bang B \to \bang (A \otimes B) \mathrlap{,}
\end{equation}
for $A, B \in \catK$, a map
\begin{equation}
\label{equ:moni}
\moni \co  \unit \to \bang  \unit \mathrlap{,}
\end{equation}
and invertible modifications with components
\begin{equation}
\label{equ:lax-monoidal-associativity}
\begin{tikzcd}[column sep = huge, ampersand replacement=\&]
\bang A \otimes \bang B \otimes \bang C \ar[r, "\id_A \otimes \monn_{B,C}"] \ar[d, "\monn_{A,B} \otimes \id_C"'] \ar[dr,phantom,"\Two\omega_{A,B,C}"] \&
\bang A \otimes \bang (B \otimes C) \ar[d, "\monn_{A, B \otimes C}"]  \\
\bang (A \otimes B) \otimes \bang C \ar[r, "\monn_{A \otimes B, C}"'] \& \bang (A \otimes B \otimes C) \mathrlap{,}
\end{tikzcd}
\end{equation}
for $A, B, C \in \catK$,
\begin{equation}
\label{equ:lax-monoidal-unitality}
\begin{tikzcd}[column sep = large, ampersand replacement=\&]
\&
\bang  \unit \otimes   \bang A
\ar[d, phantom, description, "\Two \kappa_A"]
\ar[dr, "\monn_{ \unit, A}"]   \&
\\
\unit \otimes \bang A
\ar[rr, "\id_{\bang A}"']
\ar[ur, "\mon_ \unit \otimes\id_{\bang A}"]  \&
\phantom{} \&
\bang A  \mathrlap{,}
\end{tikzcd}   \qquad
\begin{tikzcd}[column sep = large, ampersand replacement=\&]
\&
\bang A \otimes \bang  \unit
\ar[d, phantom, description, "\Two \zeta_A"]
\ar[dr, "\monn_{A,  \unit}"]   \&
\\
\bang A \otimes \unit
\ar[rr, "\id_{\bang A}"']
\ar[ur, "\id_{\bang A} \otimes \moni"]  \&
\phantom{} \&
\bang A  \mathrlap{,}
\end{tikzcd}
\end{equation}
for $A \in \catK$, and
\begin{equation}
\label{equ:lax-monoidal-braiding}
\begin{tikzcd}[ampersand replacement=\&]
\bang A \otimes \bang B \ar[r, "\mathsf{r}_{\bang A, \bang B}"] \ar[d, "\monn_{A,B}"'] \ar[dr,phantom,"\Two \theta_{A,B}"] \& \bang B \otimes \bang A \ar[d, "\monn_{B,A}"] \\
\bang (A \otimes B) \ar[r, "\bang \mathsf{r}_{A,B}"'] \& \bang (B \otimes A) \mathrlap{,}
\end{tikzcd}
\end{equation}
for $A, B \in \catK$, which satisfy the coherence conditions for a sylleptic lax monoidal pseudofunctor;
\item the comultiplication $\dig$  is  a braided  monoidal pseudonatural transformation, \ie we have an invertible modification with components
\begin{equation}
\label{equ:comultiplication-monoidal-2}
\begin{tikzcd}[column sep = large]
\bang A \otimes \bang B \ar[rr, "\monn_{A,B}"]  \ar[d, "\dig_A \otimes \dig_B"']
\ar[drr,phantom,"\Two \dig^2_{A,B}"]
& & \bang (A \otimes B) \ar[d, "\dig_{A \otimes B}"] \\
\bbang A \otimes \bbang B \ar[r, "\monn_{\bang A, \bang B}"']  & \bang ( \bang A \otimes \bang B) \ar[r, "\bang \monn_{A, B}"']  & \bbang (A \otimes B)  \mathrlap{,}
\end{tikzcd}
\end{equation}
and an invertible 2-cell
\begin{equation}
\label{equ:comultiplication-monoidal-0}
\begin{tikzcd}[column sep = large]
\unit \ar[r, "\moni"] \ar[d, "\moni"'] \ar[dr,phantom,"\Two \dig^0"] & \bang  \unit \ar[d, "\dig_ \unit"] \\
\bang  \unit \ar[r, "\bang \moni"'] & \bbang  \unit   \mathrlap{,}
\end{tikzcd}
\end{equation}
which satisfy the coherence conditions for a braided monoidal transformation;
\item the counit $\der$ is a braided monoidal pseudonatural transformation, \ie we have an invertible modification with components
\begin{equation}
\label{equ:counit-monoidal-2}
\begin{tikzcd}[column sep = large]
\bang A \otimes \bang B \ar[r, "\monn_{A,B}"]  \ar[d, "\der_A \otimes \der_B"']  \ar[dr,phantom,"\Two \der^2_{A,B}"]
& \bang (A \otimes B) \ar[d, "\der_{A \otimes B}"]  \\
A \otimes B \ar[r, "\id_{A \otimes B}"'] & A \otimes B  \mathrlap{,}
\end{tikzcd}
\end{equation}
for $A, B \in \catK$, and an invertible 2-cell
\begin{equation}
\label{equ:counit-monoidal-0}
\begin{tikzcd}
\unit \ar[r, "\moni"] \ar[d, "\id_\unit"'] \ar[dr,phantom,"\Two \der^0"] & \bang \unit \ar[d, "\der_\unit"]  \\
\unit  \ar[r, "\id_\unit"'] & \unit  \mathrlap{,}
\end{tikzcd}
\end{equation}
which satisfy the coherence conditions for a braided monoidal transformation;
\item the associativity and unitality constraints $\pi$, $\mu$, $\nu$  of the pseudocomonad are monoidal modifications.
\end{itemize}
\end{definition}

In the one-dimensional setting, it is well-known that the category of coalgebras for a symmetric monoidal comonad admits a symmetric
monoidal structure. The 2-dimensional counterpart of this
result requires some care, in that one does not get back a structure that is as strict as the one on $\catK$ from which one starts.  Let us recall the precise statement from~[66].

\begin{theorem}[Miranda] \label{thm:coalg-is-monoidal} Let $\catK$ be a symmetric Gray monoid and
let $(\bang, \dig, \der)$ be a symmetric lax monoidal pseudocomonad on $\catK$. Then
the 2-category of pseudocoalgebras $\Em{\catK}$ admits the structure of a symmetric monoidal bicategory so that
the forgetful 2-functor $U \co \Em{\catK} \to \catK$ is a strict symmetric monoidal 2-functor.
Furthermore, the associativity and unit constraints for this monoidal bicategory are 2-natural and they satisfy the pentagon and triangle axioms strictly.
\end{theorem}

We outline some of the structure implicit in the proof of \cref{thm:coalg-is-monoidal} for later use. Let $\catK$ be a symmetric Gray monoid and
let $(\bang, \dig, \der)$ be a symmetric lax monoidal pseudocomonad on $\catK$, with data as in \cref{thm:sym-lax-monoidal-pseudocomonad}.
Let $A$ and $B$ be coalgebras with structure maps $a \co A \to \bang A$
and $b \co B \to \bang B$, respectively. Their tensor product in $\Em{\catK}$ is the pseudocoalgebra with underlying object
$A \otimes B$ and structure map the following composite:
\[
\begin{tikzcd}
A \otimes B \ar[r, "a \otimes b"] & \bang A \otimes \bang B \ar[r, "\monn_{A,B}"] & \bang (A\otimes B) \mathrlap{.}
\end{tikzcd}
\]
The associativity constraint is the invertible 2-cell obtained by the following pasting diagram:
\[
\begin{tikzcd}[column sep = large]
A \otimes B \ar[r, "a \otimes b"] \ar[d, "a \otimes b"'] \ar[dr,phantom,"\Two \bar{a} \otimes \bar{b}"] &[3em]
\bang A \otimes \bang B \ar[r, "\monn_{A,B}"] \ar[d, "\dig_A \otimes \dig_B"]  \ar[ddr,phantom,"\Two \dig^2_{A,B}"]   &[3em]
\bang (A \otimes B) \ar[dd, "\dig_{A \otimes B}"] \\
\bang A \otimes \bang B \ar[r, "\bang a \otimes \bang b"] \ar[d, "\mon_{A, B}"'] \ar[dr,phantom,"\cong"] &
\bbang A \otimes \bbang B \ar[d, "\monn_{A, B}"] &  \\
\bang A \otimes \bang B \ar[r, "\bang (a \otimes b)"'] &
\bang (\bang A \otimes \bang B) \ar[r, "\bang \monn_{A, B}"'] &
\bbang (A \otimes B) \mathrlap{.}
\end{tikzcd}
\]
The unitality constraint is the invertible 2-cell below:
\[
\begin{tikzcd}[column sep = huge]
A \otimes B \ar[r, "a \otimes b"] \ar[dr,  bend right = 20, "\id_{A \otimes B}"']  &
\bang A \otimes \bang B \ar[d, "\der_A \otimes \der_B"]  \ar[r, "\monn_{A,B}"]  \ar[dr,phantom,"\Two \der^2_{A,B}"] &
\bang (A \otimes B) \ar[d, "\der_{A \otimes B}"] \\
\phantom{}
\ar[ur, phantom, pos = (0.7), "\Two \tilde{a} \otimes \tilde{b}"]
& A \otimes B \ar[r, "\id_{A \otimes B}"']  &  A \otimes B  \mathrlap{.}
\end{tikzcd}
\]
The unit of the monoidal structure is the pseudocoalgebra with underlying object $\unit$ and coalgebra structure map $\moni \co \unit \to \bang \unit$. Its associativity
and unitality constraints are given by the invertible 2-cells $\dig^0$ and $\der^0$ in~\eqref{equ:comultiplication-monoidal-0} and~\eqref{equ:counit-monoidal-0}, respectively.

A subtle point is that, even if the tensor product of $\catK$ is strictly unital and associative, the tensor product in $\Em{\catK}$ is not, even if the underlying objects of the
relevant pseudocoalgebras are equal. The key point here is that, for pseudocoalgebras $A, B, C$, the pseudocoalgebra structures on $(A \otimes B) \otimes C$ and $A \otimes (B \otimes C)$ are
isomorphic in $\Em{\catK}$. This involves making the identity map $\id_{A \otimes B \otimes C}$ into a pseudocoalgebra morphism.

\begin{remark} \label{equ:lift-braiding-to-em}
The content of \cref{thm:coalg-is-monoidal} goes much further than merely lifting tensor product and unit from $\catK$ to $\Em{\catK}$, in that it asserts that all the data for the symmetric Gray monoid $\catK$,
as in \cref{def:symmetric-gray-monoid}, lifts to $\Em{\catK}$. This means in particular that:
\begin{enumerate}
\item  the braiding $\bra_{A, B} \co A \otimes B \to B \otimes A$ is a pseudocoalgebra morphism for all pseudocoalgebras $A, B$;
\item the components $\beta^1_{A,B,C}$ and $\beta^2_{A,B,C}$ of the braiding constraints are pseudocoalgebra 2-cells for all pseudocoalgebras  $A, B, C$;
\item the component $\sigma_{A,B}$ of the syllepsis is a pseudocoalgebra 2-cell for all pseudocoalgebras $A$ and $B$.
\end{enumerate}
\end{remark}

\begin{corollary} Let $\catK$ be a symmetric Gray monoid and
$(\bang, \dig, \der)$  a symmetric lax monoidal pseudocomonad on $\catK$.
The forgetful-cofree biadjunction between $\catK$ and $\Em{\catK}$ in~\eqref{equ:em-adjunction} lifts to a symmetric lax monoidal biadjunction, as in
\[
\begin{tikzcd}[column sep = large]
(\catK, \otimes, \unit)
\ar[r, shift right =1, bend right = 10, "F"']
\ar[r, description, phantom, "\scriptstyle \bot"] &
(\Em{\catK}, \otimes, \unit)   \mathrlap{.}
\ar[l, shift right = 1, bend right = 10, "U"']
\end{tikzcd}
\]
\end{corollary}

\begin{proof} Since the left biadjoint~$U$ is a sylleptic strict monoidal pseudofunctor, the claim
follows by a two-dimensional version of Kelly's doctrinal adjunction, \cf~\cite[pages~62-63]{GarnerR:enrcfc}. In particular, the right biadjoint~$F$ becomes a sylleptic lax monoidal
pseudofunctor by~\cite[Proposition~15]{DayStreet}.
\end{proof}

For a 2-category $\catK$ and pseudocomonad $(\bang, \dig, \der)$ on it, it is immediate to observe that the components of the comultiplication $\dig_A \co \bang A \to \bbang A$ are
pseudocomonad morphisms, the pseudonaturality 2-cells
\[
\begin{tikzcd}
\bang A \ar[r, "\dig_A"] \ar[d, "\bang f"'] \ar[dr,phantom,"\Two \bar{\dig}_f"] & \bbang A \ar[d, "\bbang f"] \\
\bang B \ar[r, "\dig_B"'] & \bbang B \mathrlap{,}
\end{tikzcd}
\]
for $f \co A \to B$ in $\catK$, are pseudocoalgebra 2-cells (since $\pi$ is a modification), and the components $\pi_A$ of its associativity constraints, for $A \in \catK$,  are pseudocoalgebra 2-cells (by the
coherence axioms for a pseudocomonad). When $\catK$ is a Gray
monoid and the pseudocomonad is sylleptic lax monoidal, as in \cref{thm:sym-lax-monoidal-pseudocomonad}, other parts of the structure can also be lifted to
the 2-category of pseudocoalgebras. This is described in the next two lemmas. The second one concerns pseudocoalgebra 2-cells and therefore does not have a one-dimensional counterpart.

Let us fix a symmetric Gray monoid $\catK$ and a symmetric lax monoidal pseudocomonad $(\bang, \dig, \der)$ on it as in \cref{thm:sym-lax-monoidal-pseudocomonad}.

\begin{lemma} \label{thm:mu-are-coalgebra-morphisms} \leavevmode
\begin{enumerate}[(i)]
\item For every $A, B \in \catK$, the map $\monn_{A, B} \co \bang A \otimes \bang B \to \bang (A \otimes B)$ is a pseudocoalgebra morphism, \ie we have an invertible 2-cell
\[
\begin{tikzcd}[column sep = large]
\bang A \otimes \bang B \ar[d, "\dig_A \otimes \dig_B"'] \ar[r, "\monn_{A,B}"]
\ar[ddr, phantom, description, "\Two"]
&  \bang (A \otimes B) \ar[dd, "\dig_{A \otimes B}"]  \\
\bbang A \otimes \bbang B \ar[d, "\monn_{\bang A, \bang B}"'] & \\
\bang (\bang A \otimes \bang B) \ar[r, "\bang \monn_{A,B}"'] & \bbang (A \otimes B)
\end{tikzcd}
\]
such that the appropriate coherence conditions hold.
\item The map $\moni \co \unit \to \bang \unit$ is a pseudocoalgebra morphism, \ie we have an invertible 2-cell
\[
\begin{tikzcd}[column sep = large]
\unit \ar[r, "\moni"] \ar[dd, "\moni"']  \ar[ddr, phantom, description, "\Two"] & \bang \unit \ar[dd, "\dig_\unit"] \\
& \\
\bang \unit \ar[r, "\bang \moni"'] & \bbang \unit
\end{tikzcd}
\]
such that the appropriate coherence conditions hold.
\end{enumerate}
\end{lemma}

\begin{proof} For part~(i), the required invertible 2-cell is given by the 2-cell $\dig^2_{A,B}$ in~\eqref{equ:comultiplication-monoidal-2}. The two coherence conditions for a pseudoalgebra morphism follow from the first\footnote{{Cf.}~\cref{thm:coh-numb-convention}.}
coherence axiom of a monoidal modification for $\pi$ (the associativity constraint of the pseudocomonad) and for $\nu$ (the right unitality constraint of the pseudomonad),

For part (ii), it suffices to recall that $\moni \co \unit \to \bang \unit$ is the structure map of a pseudocoalgebra.
\end{proof}

Next, we show that the 2-cells that are part of the structure of a symmetric lax monoidal pseudomonad can also be lifted. For this statement to make sense, recall that the components of the
comultiplication $\dig_A \co \bang A \to \bbang A$, for $A \in \catK$ are pseudoalgebra morphisms, the statement of \cref{thm:mu-are-coalgebra-morphisms}, and that
the braiding $\bra_{A, B} \co A \otimes B \to B \otimes A$ is a pseudoalgebra morphism for all pseudoalgebras $A, B$ by \cref{equ:lift-braiding-to-em}.

\begin{lemma} \label{thm:to-be-added-1} \leavevmode
\begin{enumerate}
\item The 2-cell $\omega_{A, B, C}$   in \eqref{equ:lax-monoidal-associativity} is a pseudocoalgebra 2-cell for all  pseudocoalgebras $A, B, C$.
\item The 2-cells $\kappa_A$ and $\zeta_A$ in \eqref{equ:lax-monoidal-unitality} are  pseudocoalgebra 2-cells for every  pseudocoalgebra $A$.
\item The 2-cell $\theta_{A,B}$ in \eqref{equ:lax-monoidal-braiding} is a pseudocoalgebra 2-cell for all pseudoalgebras $A, B$,
\item The 2-cell $\dig^2_{A,B}$ in \eqref{equ:comultiplication-monoidal-2}  is a pseudocoalgebra 2-cell   for all pseudoalgebras $A, B$.
\item The 2-cell $\dig^0$ in \eqref{equ:comultiplication-monoidal-0} is a  pseudocoalgebra 2-cell.
\end{enumerate}
\end{lemma}

\begin{proof} For parts (i) and (ii), use the first, second and third coherence conditions for the comultiplication~$\dig$ to be a monoidal transformation to prove the claim for~$\omega_{A, B, C}$, $\kappa_A$ and $\zeta_A$,
respectively. For part~(iii), use the condition expressing that the monoidal transformation  $\dig$ is braided. For parts~(iv) and (v), use the first and second coherence coherence conditions for the modification $\pi$ (the associativity constraint of the pseudocomonad) to be monoidal, respectively.
\end{proof}

\subsection*{Linear exponential pseudocomonads}
We are now ready to introduce our bicategorical counterpart of  linear exponential comonads, which is based on the one-dimensional axiomatisation of~[47].
Note that, since the 2-category of pseudocoalgebras for a symmetric monoidal pseudocomonad $\Em \catK$ is a symmetric monoidal bicategory by~\cref{thm:coalg-is-monoidal},
we can consider braided symmetric pseudocomonoids therein, in the sense of \cref{thm:comonoid} and \cref{thm:braided-comonoid}.

\begin{definition} \label{thm:linear-exponential-comonad}
Let $\catK$ be a symmetric Gray monoid. A \myemph{linear exponential pseudocomonad} on $\catK$ is a symmetric lax monoidal pseudocomonad $(\bang, \dig, \der)$ on $\catK$
as in \cref{thm:sym-lax-monoidal-pseudocomonad} equipped with additional data as follows.
\begin{itemize}
\item For every pseudocoalgebra $A$, we have pseudocoalgebra morphisms
\begin{equation}
\label{equ:lin-exp-com-and-cou}
\com_A \co A \to  A \otimes A \mathrlap{,} \qquad
e_A \co A \to \unit \mathrlap{,}
\end{equation}
and invertible pseudocoalgebra 2-cells
\begin{gather}
\label{equ:lin-exp-associativity}
\begin{tikzcd}[column sep = large, ampersand replacement=\&]
\ar[r, "\com_A"] \ar[d, "\com_A"']
\ar[dr,phantom,"\Two \alpha_A"] \&
A \otimes A
\ar[d, "\id_A \otimes \com_A"] \\
A \otimes A
\ar[r, "\com_A \otimes \id_A"'] \&
A \otimes A \otimes A
\mathrlap{,}
\end{tikzcd}  \\
\label{equ:lin-exp-unitality}
\begin{tikzcd}[column sep = {1.5cm,between origins}, ampersand replacement=\&]
\&
A \otimes A
\ar[d, phantom, description, "\Two \lambda_A"]
\ar[dr, "e_A \otimes \id_A"]   \&
\\
\ar[ur, "\com_A"]
\ar[rr, "\id_A"']  \&
\phantom{} \&
A \otimes A \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}[column sep = {1.5cm,between origins}, ampersand replacement=\&]
\&
A \otimes A
\ar[d, phantom, description, "\Two \rho_A"]
\ar[dr, "\id_A \otimes e_A"]   \&
\\
\ar[ur, "\com_A"]
\ar[rr, "\id_A"']  \&
\phantom{} \&
A \otimes A \mathrlap{,}
\end{tikzcd} \\
\label{equ:lin-exp-braiding}
\begin{tikzcd}[column sep = {1.5cm,between origins}, ampersand replacement=\&]
\&
A \otimes A
\ar[d, phantom, description, "\Two \gamma_A"]
\ar[dr, "\bra_{A,A}"]   \&
\\
\ar[ur, "\com_A"]
\ar[rr, "\com_A"']  \&
\phantom{} \&
A \otimes A
\end{tikzcd}
\end{gather}
that equip $A$ with the structure of symmetric pseudocomonoid in $\Em{\catK}$.
\item The families of maps $(\com_A)_{A \in \catK}$ and $(e_A)_{A \in \catK}$ are pseudonatural with respect to pseudocoalgebra morphisms and pseudocoalgebra 2-cells.
\item The families of 2-cells $(\alpha_A)_{A \in \catK}$, $(\lambda_A)_{A \in \catK}$, $(\rho_A)_{A \in \catK}$ and $(\gamma_A)_{A \in \catK}$ are modifications.
\item The pseudonatural transformations $\com$ and $e$ are braided monoidal.
\item The modifications $\alpha$, $\lambda, \rho$ and $\gamma$  are monoidal.
\end{itemize}
\end{definition}

\begin{remark} \label{thm:unfold-linear-exponential}
We unfold the definition of linear exponential pseudocomonad for later use.
\begin{itemize}
\item For every pseudocoalgebra~$A$, the map $\com_A \co A \to A \otimes A$ is a pseudocoalgebra morphism, \ie we have an invertible 2-cell
\[
\begin{tikzcd}
A \ar[r, "\com_A"]  \ar[dd, "a"'] \ar[ddr, phantom, description, "\Two \bar{n}_A"] &  A \otimes  A \ar[d, "a \otimes a"]  \\
&  \bang A \otimes \bang A \ar[d, "\monn_{A, A}"]  \\
\bang A \ar[r, "\bang \com_A"'] &  \bang (A \otimes A) \mathrlap{.}
\end{tikzcd}
\]
Similarly, for each pseudocoalgebra~$A$, the map $e_A \co A \to \unit$ is a pseudocoalgebra morphism, \ie we have an invertible 2-cell
\[
\begin{tikzcd}
A \ar[r, "e_A"] \ar[d, "a"'] \ar[dr, phantom, description, "\Two \bar{e}_A"] & \unit \ar[d, "\moni"] \\
\bang A \ar[r, "\bang e_\unit"']   & \bang \unit \mathrlap{.}
\end{tikzcd}
\]
Furthermore, the 2-cells $\alpha_A$, $\rho_A$, $\lambda_A$ and $\gamma$ in \eqref{equ:lin-exp-associativity}, \eqref{equ:lin-exp-unitality}, and \eqref{equ:lin-exp-braiding} are pseudocoalgebra 2-cells with respect to this pseudocoalgebra morphisms.
\item We have invertible 2-cells making $\com$ into a pseudonatural transformation with respect to pseudocoalgebra morphisms, \ie for every pseudocoalgebra morphism $f \co A \to  B$, there is an invertible  2-cell
\begin{equation}
\label{equ:d-psdnat}
\begin{tikzcd}
A \ar[r, "\com_A"] \ar[d, "f"'] \ar[dr, phantom, description, "\Two n_f"]  &  A \otimes  A \ar[d, "f \otimes f"] \\
B \ar[r, "\com_B"'] &  B \otimes  B \mathrlap{,}
\end{tikzcd}
\end{equation}
satisfying the appropriate coherence axioms.
Similarly, we have invertible 2-cells making $e$ into a pseudonatural transformation with respect to pseudocoalgebra
morphisms, \ie  for every pseudocoalgebra morphism $f \co A \to B$,
we have an invertible 2-cell
\begin{equation}
\label{equ:e-psdnat}
\begin{tikzcd}
A \ar[r, "e_A"] \ar[d, "f"']  \ar[dr, phantom, description, "\Two e_f"]  & \unit \ar[d, "\id_\unit"] \\
B \ar[r, "e_B"'] & \unit \mathrlap{,}
\end{tikzcd}
\end{equation}
satisfying the appropriate coherence axioms.
\item We have an invertible modification $\com^2$ and an invertible 2-cell $\com^0$ making the pseudonatural transformation $\com$ into
a braided monoidal pseudonatural transformation, \ie
\begin{equation}
\label{equ:d-monoidal}
\begin{tikzcd}[column sep = large]
A \otimes B \ar[r, "\com_{A \otimes B}"] \ar[d, "\id_{A \otimes B}"'] \ar[dr, phantom, description, "\Two \com^2_{A,B}"]  & A \otimes B \otimes A \otimes B \ar[d, "\id_A \otimes \bra_{A,B} \otimes \id_B"] \\
A \otimes B \ar[r, "\com_A \otimes \com_B"'] & A \otimes A \otimes B \otimes B \mathrlap{,}
\end{tikzcd}
\qquad
\begin{tikzcd}
\unit \ar[d, "\id_\unit"'] \ar[r, "d_\unit"] \ar[dr, phantom, description, "\Two \com^0"] & \unit  \otimes \unit  \ar[d, "\id_\unit"] \\
\unit \ar[r, "\id_\unit"'] &  \unit \mathrlap{.}
\end{tikzcd}
\end{equation}
Similarly, we  have an invertible modification $e^2$ and an invertible 2-cell  $e^0$  making the pseudonatural transformation $e$ into
a braided monoidal pseudonatural transformation, \ie
\begin{equation}
\label{equ:e-monoidal}
\begin{tikzcd}[column sep = large]
A \otimes B \ar[r, "e_A \otimes e_B"] \ar[d, "\id_{A \otimes B}"'] \ar[dr, phantom, description, "\Two e^2_{A,B}"]  & \unit \ar[d, "\id_{A \otimes B}"] \\
A \otimes B \ar[r, "e_{A \otimes B}"'] & \unit \otimes \unit \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}
\unit \ar[r, "\id_\unit"] \ar[d, "\id_\unit"'] \ar[dr, phantom, description, "\Two e^0"] & \unit \ar[d, "\id_\unit"] \\
\unit \ar[r, "e_\unit"'] & \unit \mathrlap{.}
\end{tikzcd}
\end{equation}
\end{itemize}
\end{remark}

\begin{remark} \label{thm:retract-cofree}
In the one-dimensional setting, a possible axiomatisation of the notion of a linear
exponential comonad involves requiring the existence of a commutative comonoid structure only
on cofree coalgebras. From this one can derive the presence of
a commutative comonoid structure on every coalgebra, using that every coalgebra is a retract of a cofree one. We expect that a similar argument applies in the two-dimensional
setting, \cf also \cref{thm:compare-with-jacq} below, but do not pursue the details here.
\end{remark}

Let us now fix a symmetric Gray monoid $\catK$ and a linear exponential pseudocomonad $(\bang, \dig, \der)$ on it, with data as in \cref{def:psd-comonad,thm:sym-lax-monoidal-pseudocomonad,thm:linear-exponential-comonad}.

\begin{proposition} \label{thm:coalgebras-is-cartesian} Let $\catK$ be a symmetric Gray monoid and $(\bang, \dig, \der)$ be a linear exponential pseudocomonad.
The  symmetric monoidal structure on the 2-category of pseudocoalgebras $\Em{\catK}$ of \cref{thm:coalg-is-monoidal} is a cartesian monoidal structure.
In particular, $\Em{\catK}$ has finite products.
\end{proposition}

\begin{proof}  The axioms for a linear exponential pseudocomonad require every pseudocoalgebra to be a symmetric pseudocomonoid in the 2-category of pseudocoalgebras, in a pseudonatural and monoidal way, so \cref{thm:prod-iff-all-ccmon} implies the claim.
\end{proof}

\begin{remark} \label{thm:canonical-is-linear-exponential}
By the essential uniqueness of finite products,  the canonical symmetric pseudocomonoid structure on a pseudoalgebra $A$ given by products  in $\Em{\catK}$ is equivalent to the one given by the linear exponential pseudocomonad.
\end{remark}

We derive some more consequences of the axioms for a linear exponential pseudocomonad. For the next lemma, recall that if $A$ and $B$ are pseudocoalgebras, then $A \otimes B$ admits the structure of a pseudocoalgebra by \cref{thm:coalg-is-monoidal} and thus acquires the structure of a symmetric pseudocomonoid by the axioms for a linear exponential pseudocomonad.
Recall also that the 2-category $\SymCoMon{\catK}$ has a symmetric monoidal structure by \cref{thm:sym-comon-is-monoidal}.

\begin{lemma}
\label{thm:id-is-comonoid-morphism}
\leavevmode
\begin{enumerate}[(i)]
\item Let $A$ and $B$ be pseudocoalgebras. Then the symmetric pseudocomonoid  $(A \otimes B, \com_{A \otimes B}, e_{A \otimes B})$, determined by the linear
exponential pseudocomonad, is equivalent to the tensor product of the symmetric pseudocomonoids
$(A, \com_A, e_A)$ and $(B, \com_B, e_B)$ in $\SymCoMon{\catK}$.
\item The symmetric pseudocomonoid $(\unit, d_\unit, e_\unit)$ determined by the linear exponential pseudocomonad
is equivalent to the unit of $\SymCoMon \catK$.
\end{enumerate}
\end{lemma}

\begin{proof} For~(i), recall that the definition of the tensor product $(A, \com_A, e_B) \otimes (B, \com_B, e_B)$ from the comments below~\cref{thm:coalg-is-monoidal}. In particular,
its underlying object is $A \otimes B$, comultiplication as in~\eqref{equ:comultiplication-for-tensor}, and counit  as in~ \eqref{equ:counit-for-tensor}.  We claim that the identity map $\id_{A \otimes B} \co A \otimes B \to A \otimes B$ is a braided pseudocomonoid morphism
between $(A \otimes B, \com_{A \otimes B}, e_{A \otimes B})$ and $(A, \com_A, e_B) \otimes (B, \com_B, e_B)$. For this, we need 2-cells fitting in
the diagrams
\[
\begin{tikzcd}[column sep = huge]
A \otimes B \ar[r, "\id_{A \otimes B}"] \ar[dd, "\com_{A \otimes B}"']
\ar[ddr, phantom, description, "\Two"]
& A \otimes B  \ar[d, "\com_A \otimes \com_B"] \\
& A \otimes A \otimes B \otimes B \ar[d, "\id_A \otimes \mathsf{r}_{A,B} \otimes \id_B"] \\
A \otimes B \otimes A \otimes B \ar[r, "\id_{A \otimes B \otimes A \otimes B}"'] & A \otimes B \otimes A \otimes B \mathrlap{,}
\end{tikzcd}
\qquad
\begin{tikzcd}
A \otimes B \ar[r, "\id"] \ar[dd, "e_{A \otimes B}"']
\ar[ddr, phantom, description, "\Two"]
& A \otimes B \ar[d, "e_A \otimes e_B"] \\
& \unit \otimes \unit \ar[d, "\id"] \\
\unit \ar[r, "\id"'] & \unit \mathrlap{.}
\end{tikzcd}
\]
These are given by the 2-cells $\com^2_{A,B}$ and $e^2_{A,B}$ in~\eqref{equ:d-monoidal} and~\eqref{equ:e-monoidal}, which are part of the data making~$\com$ and~$e$ into braided monoidal
pseudonatural transformations, respectively. We need to check the four coherence conditions for a braided pseudocomonoid morphism. The four proofs use
the first\footnote{{Cf.} \cref{thm:coh-numb-convention}.} coherence condition for the four modifications $\alpha$, $\lambda, \rho$ and $\gamma$ in \eqref{equ:lin-exp-associativity}, \eqref{equ:lin-exp-unitality}, and \eqref{equ:lin-exp-braiding} to be monoidal, respectively.

For part~(ii), recall that the unit $\unit$ is a braided pseudocomonoid with identity maps for both comultiplication and unit, and identity 2-cells for all the constraints. We claim that the identity
map $\id_\unit \co \unit \to \unit$ is a braided pseudocomonoid morphism from $(\unit, d_\unit, e_\unit)$ to $(\unit, \id_\unit, \id_\unit)$. Thus, we need invertible 2-cells:
\[
\begin{tikzcd}[column sep = large]
\unit \ar[r, "\id_\unit"] \ar[d, "d_\unit"'] \ar[dr,phantom,"\Two"] & \unit \ar[d, "\id_\unit"] \\
\unit \otimes \unit \ar[r, "\id_\unit \otimes \id_\unit"'] & \unit \otimes \unit \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}[column sep = large]
\unit \ar[r, "\id_\unit"] \ar[d, "e_\unit"'] \ar[dr,phantom,"\Two"] & \unit \ar[d, "\id_\unit"] \\
\unit \otimes \unit \ar[r, "\id_\unit \otimes \id_\unit"'] & \unit \otimes \unit \mathrlap{.}
\end{tikzcd}
\]
These are given by the 2-cells $\com^0$ and $e^0$ in ~\eqref{equ:d-monoidal} and~\eqref{equ:e-monoidal}, respectively. To verify the four coherence conditions for a braided pseudocomonoid morphism, use
the second coherence condition for the modifications $\alpha$, $\lambda, \rho$ and $\gamma$ to be monoidal, respectively.
\end{proof}

\begin{corollary} Let $A$ and $B$ be pseudocoalgebras. The symmetric pseudocomonoid  $(A \otimes B, \com_{A \otimes B}, e_{A \otimes B})$ is the product of $A$ and $B$ in $\SymCoMon{\catK}$.
\end{corollary}

\begin{proof} Immediate from~\cref{thm:id-is-comonoid-morphism} and \cref{thm:ccmon-finprod}.
\end{proof}

We now define explicitly two pseudonatural transformations, called \emph{contraction} and \emph{weakening} following the terminology used in Linear Logic,  which will be important
for our development.
For $A \in \catK$, the cofree pseudocoalgebra $\bang A$ admits the structure of symmetric pseudocomonoid
by the axioms for a linear exponential comonad, like any pseudocoalgebra.
We define the map~$\con_A$, called \emph{contraction}, to be the comultiplication of the symmetric pseudocomonoid $\bang A$, \ie we let
\begin{equation}
\label{equ:con}
\begin{tikzcd}
\bang A  \ar[r, "\con_A"] &  \bang A \otimes \bang A
\end{tikzcd}  \quad \defeq \quad
\begin{tikzcd}
\bang A  \ar[r, "\com_{\bang A}"] &  \bang A \otimes \bang A \mathrlap{.}
\end{tikzcd}
\end{equation}
Similarly, we define the map $\weak_A$, called \emph{weakening}, to be the counit of the symmetric pseudocomonoid $\bang A$, \ie we let
\begin{equation}
\label{equ:weak}
\begin{tikzcd}
\bang A \ar[r, "\weak_A"] &  \unit
\end{tikzcd}
\quad \defeq \quad
\begin{tikzcd}
\bang A \ar[r, "e_{\bang A}"] &  \unit \mathrlap{,}
\end{tikzcd}
\end{equation}
By definition, $\con_A$ and $\weak_A$ are the components on objects of pseudonatural transformations.

% The next lemma establishes the two-dimensional counterparts of the diagrams in \cite[Definition 3.1]{FioreM:difsmi}.

\begin{samepage}
\begin{lemma} \label{thm:con-and-weak-coalgebra-maps}
\leavevmode
\begin{enumerate}
\item For every $A \in \catK$,
% \noten{This is part of Definition 3.1 of Fiore, it is the outer diagram  in (5)}
the map $\con_A \co \bang A \to \bang A \otimes \bang A$ is a pseudocoalgebra morphism, \ie we have an invertible 2-cell
\[
\begin{tikzcd}[column sep = large]
\bang A \ar[r, "\con_A"]  \ar[dd, "\dig_A"']
\ar[ddr, phantom, description, "\Two \bar{\con}_A"]
&  \bang A \otimes  \bang A \ar[d, "\dig_A \otimes \dig_A"]  \\
&  \bbang A \otimes \bbang A \ar[d, "\monn_{\bang A, \bang A}"]  \\
\bbang A \ar[r, "\bang \con_A"']  &  \bang (\bang A \otimes \bang A) \mathrlap{,}
\end{tikzcd}
\]
such that  the appropriate coherence conditions hold.
\item For every $A \in \catK$,
%\noten{This is part of Definition 3.1 of Fiore, just above (5)}
the  map $\weak_A \co \bang A \to \unit$ is pseudocoalgebra morphism, \ie we have an invertible 2-cell
\begin{equation}
\label{thm:dig-and-weak}
\begin{tikzcd}[column sep = large]
\bang A \ar[r, "\weak_A"] \ar[d, "\dig_A"'] \ar[dr, phantom, description, "\Two \bar{\weak}_A"] & \unit \ar[d, "\moni"]  \\
\bbang A \ar[r, "\bang{\weak}_A"']  & \bang \unit \mathrlap{,}
\end{tikzcd}
\end{equation}
such that  the appropriate coherence conditions hold.
\end{enumerate}
\end{lemma}
\end{samepage}

\begin{proof} By the definitions of  $\con_A$ and $\weak_A$ in \eqref{equ:con} and \eqref{equ:weak}, the claims are instances of the assertions that the components of the pseudonatural transformations~$\com$ and $e$
in~\eqref{equ:lin-exp-com-and-cou} are pseudocoalgebra morphisms, which are part of the axioms for a linear exponential pseudocomonad, \cf part~(i) of \cref{thm:unfold-linear-exponential}.
\end{proof}

The next proposition is a useful result since it allows us to leverage our earlier results on sylleptic lax monoidal pseudomonads to
exhibit a number of braided pseudocomonoid morphism and pseudocomonoid 2-cells.

\begin{proposition} \leavevmode
\label{thm:coalg-mor-comon-mor}
\begin{enumerate}
\item  Let $(A,a), (B, b)$ be pseudocoalgebras. Every pseudocoalgebra morphism $f \co (A,a) \to (B, b)$ is a braided pseudocomonoid morphism $f \co (A, \com_A, e_A) \to (B, \com_B, e_B)$.
\item Let $f \co A \to B$, $g \co A \to B$ be pseudocoalgebra morphisms. Every pseudocoalgebra 2-cell $\phi \co f \Rightarrow g$ is a pseudocomonoid 2-cell.
\end{enumerate}
\end{proposition}

\begin{proof} For (i), let $f \co (A,a) \to (B, b)$ be a pseudocoalgebra morphism. The 2-cells making $f$ into a braided pseudocomonoid morphism
are exactly the 2-cells in~\eqref{equ:d-psdnat} and \eqref{equ:e-psdnat} above. The four coherence conditions for a braided pseudocomonoid morphism
follow from the assumption that $\alpha$, $\lambda$, $\rho$ and $\gamma$ in~\eqref{equ:lin-exp-associativity}, \eqref{equ:lin-exp-unitality}, and \eqref{equ:lin-exp-braiding} are modifications, respectively.

For part~(ii), the two coherence conditions from the axiom describing the interaction between pseudonatural transformations and 2-cells for $\com$ and $e$, respectively.
Note that one has to use that $\phi$ is a pseudocoalgebra 2-cell to apply this axiom.
\end{proof}

\begin{samepage}
\begin{corollary}  \label{thm:dig-comonoid-morphism}
\leavevmode
% \noten{Only in part in Fiore. This is (3.6.3) of Ehrhard.}
\begin{enumerate}
\item For every $A \in \catK$, the  map $\dig_A \co \bang A \to \bbang A$ is
a braided pseudocomonoid morphism, \ie we have invertible 2-cells
% \noten{Inner square in equation (5) in Fiore.}
\[
\begin{tikzcd}[column sep = large]
\bang A
\ar[d, "\con_A"']
\ar[r, "\dig_A"]
\ar[dr, phantom, description, "\Two \bar{\dig}_A"] &
\bbang A
\ar[d, "\con_{\bang A}"]  \\
\bang A \otimes \bang A
\ar[r, "\dig_A \otimes \dig_A"'] &
\bbang A \otimes \bbang A \mathrlap{,}
\end{tikzcd} \qquad
% \noten{This does not seem to be in Fiore. It is the first diagram of (3.6.3) in Ehrhard.}
\begin{tikzcd}
\bang A
\ar[d, "\weak_A"']
\ar[r, "\dig_A"]
\ar[dr, phantom, description, "\Two \tilde{\dig}_A"]  &
\bbang A
\ar[d, "\weak_{\bang A}"] \\
\unit
\ar[r, "\id_\unit"'] 	&
\unit \mathrlap{,}
\end{tikzcd}
\]
such that the appropriate coherence conditions hold.
\item For every $A \in \catK$, the associativity constraint 2-cell $\pi_A$ of the pseudocomonad is a pseudocomonoid 2-cell.
\end{enumerate}
\end{corollary}
\end{samepage}

\begin{proof} For part~(i), $\dig_A \co \bang A \to \bbang A $ is the structure map of a pseudocoalgebra and so it is a pseudocoalgebra morphism.
The claim then follows by part~(i) of \cref{thm:coalg-mor-comon-mor}.
For part~(ii), $\pi_A$ is a pseudocoalgebra 2-cell and so the claim the follows by part~(ii) of  \cref{thm:coalg-mor-comon-mor}.
% The second diagram  follows also from \eqref{thm:dig-and-weak}  and monoidality of weakening.
\end{proof}

\begin{samepage}
\begin{corollary} \label{thm:mu-comonoid-morphism} \leavevmode
\begin{enumerate}[(i)]
\item For every $A, B \in \catK$, the map $\monn_{A, B} \co \bang A \otimes \bang B \to \bang (A \otimes B)$ is a braided pseudocomonoid morphism, \ie we have invertible 2-cells
\[
\begin{gathered}
\begin{tikzcd}[column sep =huge]
\bang A \otimes \bang B
\ar[r, "\monn_{A,B}"]
\ar[d, "\con_A \otimes \con_B"']
\ar[ddr, phantom, description, "\Two \bar{\mon}_{A,B}"] &
\bang (A \otimes B)
\ar[dd, "\con_{A \otimes B}"] \\
\bang A \otimes \bang A \otimes \bang B \otimes \bang B
\ar[d, "\id_A \otimes \bra_{A,B} \otimes \id_B"'] &  \\
\bang A \otimes \bang B \otimes \bang A \otimes \bang B
\ar[r, "\monn_{A,B} \otimes \monn_{A, B}"'] &
\bang (A \otimes B) \otimes \bang ( A \otimes B)  \mathrlap{,}
\end{tikzcd} \\[2ex]
\begin{tikzcd}[column sep = huge]
\bang A \otimes \bang B
\ar[r, "\monn_{A,B}"]
\ar[d, "\weak_A \otimes \weak_B"']
\ar[dr, phantom, description, "\Two \tilde{\mon}_{A,B}"] &
\bang (A \otimes B)
\ar[d, "\weak_{A \otimes B}"] \\
\unit \ar[r, "\id"'] & \unit  \mathrlap{,}
\end{tikzcd}
\end{gathered}
\]
such that the appropriate coherence conditions hold.
\item The map $\moni \co \unit \to \bang \unit$ is a braided pseudocomonoid morphism, \ie we have invertible 2-cells
\[
\begin{tikzcd}[column sep = large]
\unit
\ar[r, "\moni"]
\ar[d, "\id"']
\ar[dr, phantom, description, "\Two \bar{\mon}_\unit"] &
\bang \unit
\ar[d, "\con_\unit"]  \\
\unit \otimes \unit
\ar[r, "\moni \otimes \moni"'] &
\bang \unit \otimes \bang \unit  \mathrlap{,}
\end{tikzcd}
\qquad
\begin{tikzcd}
\unit
\ar[r, "\moni"]
\ar[d, "\id"']
\ar[dr, phantom, description, "\Two \tilde{\mon}_\unit"] &
\bang \unit
\ar[d, "\weak_\unit"] \\
\unit
\ar[r, "\id"'] &
\unit \mathrlap{,}
\end{tikzcd}
\]
such that the appropriate coherence conditions hold.
\end{enumerate}
\end{corollary}
\end{samepage}

\begin{proof} By \cref{thm:mu-are-coalgebra-morphisms} and \cref{thm:coalg-mor-comon-mor}.
\end{proof}

%The diagrams in the next proposition are the 2-dimensional counterparts of~\cite[Equation~(3.6.3)]{EhrhardT:intdll}. The first one corresponds to
% the inner/outer diagram in \cite[Equation~(5)]{FioreM:difsmi}.

\begin{corollary} \label{thm:to-be-added-2} \leavevmode
\begin{enumerate}
\item The 2-cell $\omega_{A, B, C}$  in \eqref{equ:lax-monoidal-associativity} is a pseudocomonoid 2-cell for all  pseudocoalgebras $A, B, C$.
\item The 2-cells $\kappa_A$ and $\zeta_A$ in \eqref{equ:lax-monoidal-unitality} are  pseudocomonoid 2-cells for every  pseudocoalgebra $A$.
\item The 2-cell $\theta_{A,B}$ in \eqref{equ:lax-monoidal-braiding} is a pseudocomonoid 2-cell for all pseudoalgebras $A, B$.
\item The 2-cell $\dig^2_{A,B}$ in \eqref{equ:comultiplication-monoidal-2} is a pseudocomonoid 2-cell for all pseudoalgebras $A, B$.
\item The 2-cell $\dig^0$ in \eqref{equ:comultiplication-monoidal-0}  is a  pseudocomonoid 2-cell.
\end{enumerate}
\end{corollary}

\begin{proof} By \cref{thm:to-be-added-1} and part~(ii) of \cref{thm:coalg-mor-comon-mor}.
\end{proof}

%The diagrams in the next proposition are the counterpart of one of the diagrams
%that are part of~\cite[Definition~3.1, part~4]{FioreM:difsmi}, as spelled out in part in~\cite[Equation~(7)]{FioreM:difsmi}.
%They are also in~\cite[Equation~(3.6.3)]{EhrhardT:intdll}.

Next, we establish that contraction and weakening are braided monoidal pseudonatural transformations.

\begin{proposition}
\label{thm:contraction-is-monoidal}
The contraction pseudonatural transformation, with components on objects $\con_A \co \bang A \to \bang A \otimes \bang A$, is  braided monoidal, \ie we have invertible modifications with components
\[
\begin{gathered}
\begin{tikzcd}[column sep = 2.5cm]
\bang A \otimes \bang B
\ar[rr, "\monn_{A, B}"]
\ar[d, "\con_A \otimes \con_B"']
\ar[drr, phantom, description, "\Two \con^2_{A,B}"]  &
\bang (A \otimes B)
\ar[d, "\con_{A \otimes B}"] \\
\bang A \otimes \bang A \otimes \bang B \otimes \bang B
\ar[r, "\id_{\bang A} \otimes \bra_{\bang A, \bang B} \otimes \id_{\bang B}"']  &
\bang A \otimes \bang B \otimes \bang A \otimes \bang B
\ar[r, "\monn_{A,B} \otimes \monn_{A,B}"'] &
\bang (A \otimes B) \otimes \bang (A \otimes B) \mathrlap{,}
\end{tikzcd} \\[1ex]
\begin{tikzcd}[column sep = large]
\unit
\ar[r, "\moni"]
\ar[d, "\id"]
\ar[dr, phantom, description, "\Two \con^0"] &
\bang \unit\ar[d, "\con_{\unit}"]  \\
\unit \otimes \unit
\ar[r, "\moni \otimes \moni"'] &
\bang \unit \otimes \bang \unit \mathrlap{,}
\end{tikzcd}
\end{gathered}
\]
such that the appropriate coherence conditions hold.
\end{proposition}

\begin{proof} By definition $\con$ is obtained by whiskering the sylleptic lax monoidal pseudofunctor $\bang$ and the braided monoidal natural transformation $\com$ and therefore it is a braided monoidal natural transformation.
Explicitly, the 2-cells $\con^2_{A,B}$ are part of the data making $\monn_{A,B}$ into a comonoid morphism in part~(i) of \cref{thm:mu-comonoid-morphism} and the 2-cell $\con^0$ is part
of the data making $\moni$ into a comonoid morphism in part~(ii) of \cref{thm:mu-comonoid-morphism}.
\end{proof}

%The next proposition is the counterpart of part of \cite[Equation~(4)]{FioreM:difsmi} and
% in \cite[Equation~(3.6.3)]{EhrhardT:intdll}.
%Part~(i) is spelled out as \cite[Equation~(6)]{FioreM:difsmi}.

\begin{proposition}
\label{thm:weakening-is-monoidal}
%  \noten{This is part of (4) in Definition 3.1 of Fiore. It is (3.6.1) in Ehrhard.}
The weakening pseudonatural transformation, with components on objects $\weak_A \co \bang A \to \unit$ is
braided monoidal, \ie we have invertible modifications with components
% \noten{This is spelled out in part as equation (6) in Fiore.}
\[
\begin{tikzcd}
\bang A \otimes \bang B
\ar[r, "\monn_{A,B}"]
\ar[d, "\weak_A \otimes \weak_B"']
\ar[dr, phantom, description, "\Two \weak^2_{A,B}"] &
\bang (A \otimes B)
\ar[d, "\weak_{A \otimes B}"] \\
\unit \otimes \unit
\ar[r, "\id_\unit"'] &
\unit  \mathrlap{,}
\end{tikzcd} \qquad
\begin{tikzcd}
\unit
\ar[d, "\id_\unit"']
\ar[r, "\moni"]
\ar[dr, phantom, description, "\Two \weak^0"]&
\bang \unit
\ar[d, "\moni"] \\
\unit
\ar[r, "\id_\unit"']  &
\unit  \mathrlap{,}
\end{tikzcd}
\]
such that the appropriate coherence conditions hold.
\end{proposition}

\begin{proof} By definition, the pseudonatural transformation $\weak$ is obtained by whiskering the sylleptic lax monoidal pseudofunctor $\bang$ and the braided monoidal pseudonatural transformation $e$. Therefore, it is
braided monoidal. The 2-cells also be given explicitly using \cref{thm:mu-comonoid-morphism}.
\end{proof}

\begin{remark} \label{thm:compare-with-jacq} Our axioms for a linear exponential pseudocomonad imply those in \cite[Definition~90]{JacqC:catcnis}.
Indeed, for each object $A \in \catK$, the object $\bang A$ is a symmetric pseudocomonoid, the maps
$\con_A \co \bang A \to \bang A \otimes \bang A$ and $\weak_A \co \bang A \to \unit$ are pseudocoalgebra morphisms by \cref{thm:con-and-weak-coalgebra-maps},
and $\dig_A \co \bang A \to \bbang A$ is a morphism of braided pseudocomonoids by \cref{thm:dig-comonoid-morphism}. We have not checked yet whether the
the converse implication holds.
\end{remark}

\subsection*{Cofree symmetric pseudocomonoids and linear exponential pseudocomonads} We now provide a method to construct linear exponential pseudocomonads
in the sense of \cref{thm:linear-exponential-comonad}, which we will use in our application in \cref{sec:prof}. We begin by considering the setting of a symmetric Gray monoid~$\catK$ and assume that it
admits the construction of cofree symmetric pseudocomonoids, in the sense that the forgetful 2-functor $U \co \SymCoMon{\catK} \to \catK$ has a right biadjoint~$F$, mapping
an object~$A \in \catK$ to the cofree symmetric pseudocomonoid on it, as in
\begin{equation}
\label{equ:cofree-ccmon}
\begin{tikzcd}[column sep = large]
\catK
\ar[r, shift left =2, "F"]
\ar[r, description, phantom, "\scriptstyle \top"]
\SymCoMon{\catK}   \mathrlap{.}
\ar[l, shift left = 2, "U"]
\end{tikzcd}
\end{equation}
Assuming further that the biadjunction in \eqref{equ:cofree-ccmon} is comonadic, in the sense that the canonical comparison 2-functor $K$ in
\[
\begin{tikzcd}[column sep = {2cm,between origins}]
\SymCoMon{\catK} \ar[rr, pos = (.4), "K"] \ar[dr, "U"'] & & \Em{\catK} \ar[dl, "U"] \\
& \catK &
\end{tikzcd}
\]
is a biequivalence, we obtain a linear exponential pseudocomonad, as stated in the next result.

\begin{theorem}
\label{thm:case-1}
Let $\catK$ be a symmetric Gray monoid. Assume that~$\catK$ admits the construction of cofree symmetric pseudocomonoids and that $\SymCoMon{\catK}$
is comonadic over $\catK$. Then the pseudocomonad on~$\catK$ determined by the forgetful-cofree biadjunction  in \eqref{equ:cofree-ccmon} is a linear exponential pseudocomonad.
\end{theorem}

\begin{proof} By \cref{thm:ccmon-finprod}, the symmetric
monoidal structure of $\catK$ lifts to $\SymCoMon{\catK}$ in such a way that the forgetful 2-functor $U \co \SymCoMon{\catK} \to \catK$ is  a strict sylleptic monoidal 2-functor.
Therefore its right biadjoint is automatically sylleptic lax monoidal by~\cite[Proposition~15]{DayStreet} and we obtain a symmetic lax monoidal pseudocomonad $\bang (-) \co \catK \to \catK$ by
a 2-categorical version of doctrinal adjunction~\cite[pages~62-63]{GarnerR:enrcfc}.
By comonadicity, $\Em{\catK}$ inherits finite products from $\SymCoMon{\catK}$. Thus, every pseudocoalgebra admits a canonical comonoid structure and the required
pseudonaturality axioms hold, because they hold trivially in $\SymCoMon{\catK}$.
\end{proof}

Our applications in \cref{sec:prof} involve a special case of \cref{thm:case-1} which we isolate for later reference. Let us now consider a symmetric Gray monoid $\catK$ that is compact closed, in the sense of~[74], and assume that it admits the construction of free symmetric pseudomonoids, in the sense that the forgetful 2-functor $U \co \CoMon{\catK} \to \catK$ has a left biadjoint $F$, as in
\begin{equation}
\label{equ:free-mon}
\begin{tikzcd}[column sep = large]
\catK
\ar[r, shift left =2,  "F"]
\ar[r, description, phantom, "\scriptstyle \bot"]
\CoMon{\catK} \mathrlap{.}
\ar[l,shift left = 2,  "U"]
\end{tikzcd}
\end{equation}
Assuming further that the biadjunction in~\eqref{equ:free-mon} is monadic, we obtain again a linear exponential pseudocomonad, as stated in the final result of this section.

\begin{theorem}
\label{thm:case-2}
Let $\catK$ be a compact closed symmetric Gray monoid. Assume that $\catK$ admits the construction of free symmetric pseudomonoids and that $\CoMon{\catK}$
is monadic over $\catK$. Then the pseudocomonad $\bang(-) \co \catK \to \catK$ determined by duality from the pseudomonad $\wn(-) \co \catK \to \catK$ determined by the
forgetful-free biadjunction in~\eqref{equ:free-mon} is a linear exponential pseudocomonad.
\end{theorem}

\begin{proof} By the dual of \cref{thm:case-1}, the pseudomonad $\wn(-) \co \catK \to \catK$ is what we may call a linear exponential pseudomonad, \ie the dual notion of that of
a linear exponential pseudocomonad.

We can then exploit the duality that is available in compact closed bicategories to turn this linear exponential pseudomonad $\wn(-) \co \catK \to \catK$ into a linear exponential
pseudocomonad $\oc (-) \co \catK \to \catK$, as desired. For example, we define
\begin{equation}
\label{equ:wn-to-bang}
\bang A \defeq \big( \wn (A^\bot) \big)^\bot \mathrlap{,}
\end{equation}
for $A \in \catK$.
\end{proof}

The linear exponential comonad constructed in \cref{thm:case-2} may be seen as counterpart of the notion of a bi-exponential in \cite[Section~2.2]{HylandM:gluoml}.
Note that the application of \cref{thm:case-1} and \cref{thm:case-2} requires to check the appropriate comonadicity or monadicity assumptions. For this, one can appeal
to the existing  monadicity results for pseudomonads~[17, 46] or, as we shall do in \cref{sec:prof}, proceed by direct inspection.

\section{Products and the Seely equivalences}
\label{sec:products}

We continue to work with our fixed symmetric Gray monoid $\catK$, but now we assume also that $\catK$ has finite products (in a bicategorical sense, following the convention set in \cref{sec:prelim}).
Recall that we write $A \with B$ for the binary product of $A, B \in \catK$, with projections $\pi_1 \co A \with B \to A$ and $\pi_2 \co A \with B \to B$,
and $\term$ for the terminal object.  Let us also fix a linear exponential pseudocomonad $(\bang, \dig, \der)$ on $\catK$ as in~\cref{thm:linear-exponential-comonad}.
The next theorem relates the cartesian and monoidal structures on~$\catK$. Its proof was suggested by the observation in~[37]
that  the Seely equivalences arise in a canonical way.

\begin{theorem}  \label{thm:seely-equivalences-monoidal}
The 2-functor $\bang(\arghole) \co \catK \to \catK$ admits the structure of a sylleptic strong monoidal 2-functor
\[
(\bang, \seell, \seeli)  \co (\catK, \with, \term)   \to  (\catK, \otimes, \unit) \mathrlap{.}
\]
\end{theorem}

\begin{proof} Since the pseudocomonad is lax monoidal, the 2-category of pseudocoalgebras $\Em{\catK}$ admits a symmetric monoidal structure by~\cref{thm:coalg-is-monoidal}. Since the pseudocomonad is a linear exponential pseudocomonad, the monoidal structure on $\Em{\catK}$ is cartesian by~\cref{thm:coalgebras-is-cartesian}. Therefore the product  of two cofree pseudocoalgebras is their tensor
product, with its evident induced pseudocoalgebra structure.

Let us now consider the biadjunction~in~\eqref{equ:em-adjunction} between $\catK$ and $\Em{\catK}$, where the left biadjoint is the forgetful 2-functor and the right biadjoint $F$ sends an object of $\catK$ to the cofree pseudocoalgebra on it. Since right biadjoints preserve products, the evident maps
\begin{equation}
\label{equ:seely-key}
f_{A,B} \co F(A \with B) \to FA \otimes FB \mathrlap{,} \qquad f \co F(\term) \to \unit \mathrlap{,}
\end{equation}
are equivalences. Since $F \co (\catK, \with, \term) \to (\Em{\catK}, \otimes, \unit)$ preserves finite products, it is a sylleptic strong monoidal pseudofunctor
between the cartesian monoidal structures, \cf [16]. The forgetful pseudofunctor $U$ is a sylleptic strict monoidal pseudofunctor $U \co (\Em{\catK}, \otimes, \unit) \to (\catK, \otimes, \unit)$
by~\cref{thm:coalg-is-monoidal} and therefore the composite,
\[
\begin{tikzcd}
(\catK, \with, \top) \ar[r, "F"] &
(\Em{\catK}, \otimes, \unit) \ar[r, "U"] &
(\catK, \otimes, \unit) \mathrlap{,}
\end{tikzcd}
\]
is a sylleptic strong monoidal pseudofunctor. But this is exactly the underlying pseudofunctor of the pseudocomonad, as desired.
\end{proof}

We can unfold explicitly the definition of the constraints of the sylleptic strong monoidal 2-functor of \cref{thm:seely-equivalences-monoidal}, which we call
\emph{Seely equivalences}, since they are the 2-categorical counterparts of the Seely
These have the form
\begin{equation}
\label{equ:seely-maps}
\seell_{A, B} \co \bang A \otimes \bang B \to \bang (A \with B) \mathrlap{,} \qquad \seeli \co I \to \bang \top \mathrlap{.}
\end{equation}
The map $\seel_{A,B}$ is the transpose of
\[
\begin{tikzcd}
\bang A \otimes \bang B \ar[r, "(\der_A \otimes \weak_B {,} \weak_A \otimes \der_B)"]  &[5em]
(A \otimes \unit) \with (\unit \otimes B) \ar[r, "\id"] &
A \with B  \mathrlap{,}
\end{tikzcd}
\]
across the biadjunction in~\eqref{equ:em-adjunction}, \ie the image of this map under the adjoint equivalence
\[
\catK[\bang A \otimes \bang B, A \with B] \simeq \Em{\catK}[ \bang A \otimes \bang B,  \bang (A \with B)] \mathrlap{.}
\]
Thus, it is the essentially unique\footnote{{Cf.}~comments below~\eqref{equ:aux-equiv}.} pseudocoalgebra morphism from $\bang A \otimes \bang B$ to $\bang (A \with B)$ with an invertible to 2-cell in
\[
\begin{tikzcd}[column sep = large]
\bang A \otimes \bang B \ar[r, "\seell_{A,B}"] \ar[dr, bend right = 20,  {pos=.4}, "(\der_A \otimes \weak_B {,} \weak_A \otimes \der_B)"'] & \bang (A \with B)
\ar[d, "\der_{A \with B}"] \\
\phantom{} \ar[ur, phantom, {pos=.7},  "\Two"] 	& A \with B \mathrlap{.}
\end{tikzcd}
\]
Using the definition in~\eqref{equ:unfold-f-sharp}, we obtain that $\seell_{A,B}$ is the composite
\[
\begin{tikzcd}
\bang A \otimes \bang B
\ar[r, "\dig_A \otimes \dig_B"] &[2em]
\bbang A \otimes \bbang B
\ar[r, "\monn_{\bang A, \bang B}"] &
\bang (\bang A \otimes \bang B)
\ar[r, "\bang (\der_A \otimes \weak_B {,} \weak_A \otimes \der_B)"] &[5em]
\bang ( (A \otimes \unit) \with (\unit \otimes B) )
\ar[r, "\id"] &
\bang (A \with B) \mathrlap{.}
\end{tikzcd}
\]
Furthermore, the adjoint quasi-inverse  ${\seell}^\bullet_{A,B}$ of $\seell_{A,B}$ is the canonical map $f_{A,B}$ in~\eqref{equ:seely-key}, \ie
\[
\begin{tikzcd}[column sep = large]
\bang (A \with B) \ar[r, "\con_{A \with B}"] &
\bang (A \with B) \otimes \bang (A \with B) \ar[r, "\bang \pi_1 \otimes \bang \pi_2"] &
\bang A \otimes \bang B \mathrlap{.}
\end{tikzcd}
\]
Similarly, $\seeli \co \unit \to \bang \term$ is the essentially unique pseudocoalgebra morphism from $I$ to $\bang \term$ with an invertible 2-cell in
\[
\begin{tikzcd}[column sep = large]
\unit \ar[r, "\seeli"] \ar[dr, bend right = 20] & \bang \top
\ar[d, "\der_\top "] \\
\phantom{} \ar[ur, phantom, {pos=.7},  "\Two"] 	& \top \mathrlap{.}
\end{tikzcd}
\]
Thus, it is the composite
\[
\begin{tikzcd}
\unit
\ar[r, "\moni"] &
\bang \unit
\ar[r] &
\bang \term \mathrlap{.}
\end{tikzcd}
\]
and its adjoint quasi-inverse ${\seel}^\bullet$ is  $\weak_\term \co \bang \term \to \unit$.

%These are exactly the formulas in~\cite[p.~170]{FioreM:difsmi} and their strong monoidality
%is mentioned just below~\cite[Definition~3.2]{FioreM:difsmi} and in \cite[Equations~(73), (74) and (75)]{MelliesPA:catsll}.

% In the next proposition, part~(i) is the counterpart of \cite[Proposition~3.1]{FioreM:difsmi} and part~(ii) is  to prove part~(ii) of \cref{thm:cocontraction-coweakeneing-with-digging}.

\begin{corollary}  \label{thm:lift-bang-to-comonoids}  \leavevmode
The 2-functor $\bang(-) \co \catK \to \catK$ lifts to 2-categories of symmetric pseudocomonoids, as in
\[
\begin{tikzcd}
\SymCoMon{\catK, \with, \term} \ar[r, "\bang"] \ar[d] & \SymCoMon{\catK, \otimes, \unit} \ar[d] \\
\catK \ar[r, "\bang"'] &
\catK \mathrlap{.}
\end{tikzcd}
\]
\end{corollary}

\begin{proof} The 2-functor is sylleptic strong monoidal by \cref{thm:seely-equivalences-monoidal}
and therefore it lifts to 2-categories of symmetric pseudocomonoids by \cite[Proposition~16]{DayStreet}.
\end{proof}

We turn to study the lifted 2-functor of \cref{thm:lift-bang-to-comonoids}. Our goal is to show  that it preserves finite products, which will be achieved in \cref{thm:lift-preserves-products}.
Let us begin with a couple of lemmas.

\begin{lemma} \leavevmode \label{thm:coh-digging-with-m}
\begin{enumerate}[(i)]
\item For every $A, B \in \catK$, the map $\seell_{A,B} \co \bang A \otimes \bang B \to \bang(A \with B)$ is a pseudocoalgebra morphism, \ie we have an invertible 2-cell
\[
\begin{tikzcd}[column sep = large]
\bang A \otimes \bang B
\ar[r, "\seell_{A,B}"]
\ar[d, "\dig_A \otimes \dig_B"']
\ar[ddr, phantom, description, "\Two \bar{\seel}^2_{A,B}"] &
\bang (A \with B)
\ar[dd, "\dig_{A \with B}"] \\
\bbang A \otimes \bbang B
\ar[d, "\monn_{\bang A, \bang B}"'] &
\\
\bang (\bang A \otimes \bang B)
\ar[r, "\bang \seell_{A,B}"'] &
\bbang (A \with B)
\end{tikzcd}
\]
which satisfies the appropriate coherence conditions.
\item The map $\seeli \co \unit \to \bang \term$ is a pseudocoalgebra morphism,  \ie we have an invertible 2-cell
\[
\begin{tikzcd}
\unit
\ar[r, "\seeli"]
\ar[d, "\moni"']
\ar[dr, phantom, description, "\Two \bar{\seel}^0"] &
\bang \term
\ar[d, "\dig_{\term}"] \\
\bang \unit
\ar[r, "\bang \seeli"'] &
\bbang \term
\end{tikzcd}
\]
which satisfies the appropriate coherence conditions.
\end{enumerate}
\end{lemma}

\begin{proof}  The Seely equivalences are, by construction, pseudocoalgebra morphisms. However, we can also provide an explicit definition of the required invertible 2-cells.
For part~(i), this is constructed as follows:
\[
\begin{tikzcd}[column sep = large]
% Row 1
\bang A \otimes \bang B
\ar[r, "\dig_A \otimes \dig_B"]
\ar[d, "\dig_A \otimes \dig_B"']
\ar[dr, phantom, description, "\Two \pi_A \otimes \pi_B"] &
\bbang A \otimes \bbang B
\ar[r, "\monn_{\bang A, \bang B}"]
\ar[d, "\dig_{\bang A} \otimes \dig_{\bang B}"]
\ar[ddr, phantom, description, "\Two \dig^2_{\bang A, \bang B}"] &
\bang  ( \bang A \otimes \bang B)
\ar[rr, " \bang (\der_A \otimes \weak_B {,} \weak_A \otimes \der_B) "]
\ar[dd, "\dig_{\bang A \otimes \bang B}"]
\ar[ddrr, phantom, description, "\cong"]&
\bang (A \with B)
\ar[dd, "\dig_{A \with B}"] \\
% Row 2
\bbang A \otimes \bbang B
\ar[r, "\bang \dig_A \otimes \bang \dig_B"]
\ar[d,  "\monn_{\bang A, \bang B}"']
\ar[dr, phantom, description, "\cong"] &
\bbbang A \otimes \bbbang B
\ar[d, "\monn_{\bbang A, \bbang B}"] &
\\
% Row 3
\bang (\bang A \otimes \bang B)
\ar[r, "\bang (\bang \dig_A \otimes \bang \dig_B)"'] &
\bang (\bbang A \otimes \bbang B)
\ar[r, "\bang \monn_{\bang A, \bang B}"'] &
\bbang (\bang A \otimes \bang B)
\ar[rr, "\bbang (\der_A \otimes \weak_B {,} \weak_A \otimes \der_B)"'] &
\bbang (A \with B) \mathrlap{.}
\end{tikzcd}
\]
For part~(ii), the required invertible 2-cells is given by
\[
\begin{tikzcd}[column sep = large]
\unit \ar[r, "\moni"] \ar[d, "\moni"']
\ar[dr, phantom, description, "\Two \dig^0"]
& \bang \unit \ar[d, "\dig_\unit"] \ar[r] \ar[dr, phantom, description, "\cong"]& \bang \term \ar[d, "\dig_\term"] \\
\bang \unit \ar[r, "\bang \moni"'] & \bbang \unit \ar[r] & \bbang \term \mathrlap{.}
\end{tikzcd}
\]
Here, $\dig^0$ is the 2-cell that is part of the data making $\mathsf{p}$ into a symmetric monoidal pseudocomonad, as
in part~(ii) of \cref{thm:sym-lax-monoidal-pseudocomonad}, and the other 2-cell is part of the pseudonaturality of $\dig$.
\end{proof}

\begin{lemma} \label{thm:seely-equiv-comonoid} \leavevmode
\begin{enumerate}
\item For every $A, B \in \catK$, the Seely equivalence $\seell_{A,B}  \co \bang A \otimes \bang B \to \bang(A \with B)  $ is a  symmetric pseudocomonoid morphism.
\item The Seely equivalence $\seeli \co \unit \to \bang \term$ is a symmetric pseudocomonoid morphism.
\end{enumerate}
\end{lemma}

\begin{proof} Both claims follow by combining  \cref{thm:id-is-comonoid-morphism}, \cref{thm:coalg-mor-comon-mor} and \cref{thm:coh-digging-with-m}.
\end{proof}

\begin{proposition} \label{thm:lift-preserves-products}
The lifted 2-functor $\bang (-) \co \SymCoMon{\catK, \with, \term} \to   \SymCoMon{\catK, \otimes, \unit}$ preserves
finite products.
\end{proposition}

\begin{proof}
Recall that finite products in 2-categories of  symmetric pseudocomonoids is given by the tensor product of their underlying objects. Therefore, we need to show that if $A$ and $B$
are symmetric pseudocomonoids with respect to $\with$, the symmetric pseudocomonoid $\bang (A \with B)$ is equivalent to the symmetric pseudocomonoid $\bang A \otimes \bang B$
in~$\SymCoMon{\catK}$ and that the symmetric pseudocomonoid $\bang \term$ is equivalent to the symmetric pseudocomonoid $\unit$.
These claims follow by  \cref{thm:seely-equiv-comonoid}.
\end{proof}

The next proposition, which will be needed for \cref{thm:bang-A-bialgebra}, describes the action of the lifted pseudofunctor of \cref{thm:lift-bang-to-comonoids} in terms of the linear exponential pseudocomonad.
For this, recall from \cref{thm:prod-iff-all-ccmon} that  the finite products of $\catK$ determine a symmetric pseudocomonoid  structure on every object of $\catK$.

% The 2-cells constructed are the counterparts of~\cite[Equations~(8) and (9)]{FioreM:difsmi}, stated in terms of $\seell$ and $\seeli$.

\begin{proposition} \label{thm:comm-comonoids-coincide}
Let $A \in \catK$. The following are equivalent as  symmetric pseudocomonoids in $(\catK, \otimes, \unit)$:
\begin{enumerate}
\item the symmetric pseudocomonoid  on $\bang A$ obtained by
applying the sylleptic strong monoidal 2-functor of \cref{thm:seely-equivalences-monoidal} to the symmetric pseudocomonoid on~$A$ determined by the finite products in~$\catK$,
\item  the symmetric pseudocomonoid on $\bang A$ determined by the linear exponential pseudocomonad.
\end{enumerate}
the identity is a braided pseudocomonoid morphism, \ie we have invertible 2-cells
\[
\begin{tikzcd}
\bang A
\ar[r, "\id"]
\ar[d, "\bang \Delta_A"']
\ar[ddr, phantom, description, "\Two"]
\bang A
\ar[dd, "\con_A"]
\\
\bang (A \with A)
\ar[d, "(\seell_{A,A})^{\bullet}"']
\\
\bang A \otimes \bang A
\ar[r, "\id"'] &
\bang A \otimes \bang A
\end{tikzcd} \qquad
\begin{tikzcd}
\bang A
\ar[r, "\id"]
\ar[d]
\ar[ddr, phantom, description, "\Two"] &
\bang A
\ar[dd, "\weak_A"] \\
\bang \term
\ar[d, "(\seeli)^\bullet"'] &
\\
\unit
\ar[r, "\id"'] &
\unit  \mathrlap{,}
\end{tikzcd}
\]
satisfying coherence conditions.
\end{proposition}

\begin{proof} Since the cofree pseudocoalgebra 2-functor $F \co \catK \to \Em{\catK}$ is a right biadjoint, it preserves finite products. Thus, the claim follows from~\cref{thm:canonical-preserved}
via \cref{thm:canonical-is-linear-exponential} and the definition of $\con_A$ and $\weak_A$. Explicitly, the required 2-cell in the  left-hand diagram can be obtained as the pasting diagram
\[
\begin{tikzcd}[column sep = huge]
\bang A
\ar[r, "\bang \Delta_A"]
\ar[d, "\con_A"']
\ar[dr, phantom, description, "\Two \bar{\con}_{\Delta_A}"] &[3em]
\bang (A \with A)
\ar[d, "\con_{A \with A}"] \\
\bang A \otimes \bang A
\ar[r, "\bang \Delta_A \otimes \bang \Delta_A"]
\ar[dr, bend right = 10, "\id_{\bang A \otimes \bang A}"']&
\bang (A \with A) \otimes \bang (A \with A)
\ar[d, "\bang \pi_1 \otimes \bang \pi_2"] \\
\phantom{} \ar[ur, phantom, {pos=.7},  "\Two"] 	&
\bang A \otimes \bang A  \mathrlap{,}
\end{tikzcd}
\]
where the invertible 2-cell in the rectangle is given by pseudonaturality of $\con$ and the
invertible 2-cell
in the triangle is obtained by the cartesian structure. For the right-hand diagram,
unfolding the definitions, we need an invertible 2-cell
\[
\begin{tikzcd}
\bang A
\ar[r]
\ar[d, "\weak_A"']
\ar[dr, phantom, description, "\Two"]&
\bang \term
\ar[d, "\weak_\term"] \\
\unit
\ar[r, "\id_\unit"'] &
\unit \mathrlap{,}
\end{tikzcd}
\]
which  is simply given by the pseudonaturality of $\weak$.
\end{proof}

The final result of this section, \cref{thm:coKleisli-cartesian-closed} below,  is the two-dimensional counterpart of a fundamental
theorem on linear exponential comonads on symmetric monoidal categories with finite
products~[64]. In its statement, by a closed symmetric Gray monoid $\catK$, we mean
that, for every $A \in \catK$, the 2-functor $(-) \otimes A \co \catK \to \catK$ has a right
biadjoint. The action of such a right biadjoint on $B \in \catK$ will be written $A \linhom B$,
using again notation inspired by Linear Logic.

\begin{theorem} \label{thm:coKleisli-cartesian-closed} Assume that $\catK$ is closed and has finite products.
Then the Kleisli bicategory $\Kl{\catK}$ is a cartesian closed bicategory.
\end{theorem}

\begin{proof} The existence of finite products in $\Kl{\catK}$ was recalled in \cref{thm:coKleisli-cartesian}. For the closed structure,
the claim follows  by~\cite[Theorem~14]{JacqC:catcnis} since the axioms for a linear exponential pseudocomonad in \cite[Definition~90]{JacqC:catcnis}  are consequences
of the axioms for a linear exponential pseudocomonad used here, as noted in \cref{thm:compare-with-jacq}. Explicitly,
the exponential of $A, B$ in $\Kl \catK$ is defined by $A \Rightarrow B = \bang A \multimap B$. Indeed, we have the following chain of equivalences:
\begin{align*}
\Kl \catK[ X \with A, B] & = \catK[ \bang ( X \with A), B ] \\
& \simeq \catK[ \bang X \otimes \bang A, B] \\
& \simeq \catK[ \bang X,  \bang A \multimap B ] \\
& = \Kl \catK[ X, A \Rightarrow B] \mathrlap{,}
\end{align*}
which can be proved to be pseudonatural.
\end{proof}

\begin{remark} \label{thm:compact-closed-hom}
In preparation for our applications in \cref{sec:prof}, we consider the special case where $\catK$ is compact closed, in the sense of~[74]. We write  $A^\perp$ for the dual of an object $A \in \catK$. The internal hom of the closed structure is defined by letting $A \multimap B \defeq A^\perp \otimes B$. Therefore, the exponential objects in $\Kl \catK$ are given
by $A \Rightarrow B \defeq \bang(A^\perp) \otimes B$.
\end{remark}

\begin{remark}  \label{thm:mellies-2-cell} We conjecture that the Kleisli biadjunction in~\eqref{equ:cokleisliadjunction} becomes a symmetric lax monoidal adjunction
when $\catK$ is considered as a symmetric Gray monoid with respect to $\otimes$, and $\Kl{\catK}$ is considered as a symmetric monoidal bicategory with respect
to $\with$, as in
\begin{equation*}
\begin{tikzcd}[column sep = large]
(\Kl{\catK}, \with, \term)
\ar[r, shift left =1, bend left =10, "K"]
\ar[r, description, phantom, "\scriptstyle \bot"] &
(\catK, \otimes, \unit) \mathrlap{.}
\ar[l, shift left = 1, bend left =10, "J"]
\end{tikzcd}
\end{equation*}
By the 2-categorical counterpart of Kelly's doctrinal adjunction theorem (see ~\cite[pages~62-63]{GarnerR:enrcfc} and~\cite[Propositions~2, 12 and~15]{DayStreet}), it is sufficient to show that
the left biadjoint $K$ is symmetric strong monoidal. This involves showing that the Seely equivalences $\seell$ are pseudonatural with respect to Kleisli maps. The candidate pseudonaturality 2-cells can be constructed as in \cite[Section~7.3.0.6]{MelliesPA:catsll}, making
essential use of invertible 2-cells of the form
\begin{equation}
\label{equ:mellies-2-cell}
\begin{tikzcd}[column sep = large]
\bang A \otimes \bang B
\ar[r, "\seell_{A,B}"]
\ar[dd, "\dig_A \otimes \dig_B"']
\ar[ddr, phantom, description, "\Two \sigma_{A, B}"]
\bang (A \with B)
\ar[d, "\dig_{A \with B}"]
\\
\bbang (A \with B)
\ar[d, "\bang {(\bang \pi_1, \bang \pi_2)}"]
\\
\bbang A \otimes \bbang B
\ar[r, "\seell_{\bang A, \bang B}"']
\bang (\bang A \with \bang B) \mathrlap{.}
\end{tikzcd}
\end{equation}
These can in turn be constructed using part~(i) of \cref{thm:coh-digging-with-m}.
As yet we have not fully verified the pseudonaturality conditions.
\end{remark}

% Section 6

\section{Biproducts, cocontraction and coweakening}
\label{sec:biproducts}

Let $\catK$ be a symmetric Gray monoid. We now assume that $\catK$ has biproducts, in the sense of \cref{thm:biproducts}. Recall that we write $A \oplus B$ for the
biproduct of $A, B \in \catK$ and $0$ for the zero object.  As a consequence of having biproducts, $\catK$  admits a form of enrichment
over the category of symmetric monoidal categories. In particular, for every $A, B \in \catK$,
the hom-category $\catK[A, B]$ admits a symmetric monoidal structure, which we call
\emph{convolution},  in analogy with the one-dimensional case.
For $f \co A \to B$ and $g \co A \to B$, we define their convolution $f + g \co A \to B$ as the composite
\begin{equation}
\label{equ:convolution}
\begin{tikzcd}
\ar[r, "\Delta_A"] &
A \oplus A
\ar[r, "f \oplus g"] &
B \oplus B
\ar[r, "\nabla_A"] &
B \mathrlap{.}
\end{tikzcd}
\end{equation}
The unit of the symmetric monoidal structure is the \emph{zero morphism} $0_{A,B} \co A \to B$
defined as the composite
\begin{equation}
\label{equ:zero-map}
\begin{tikzcd}
\ar[r] &
\ar[r] &
B \mathrlap{.}
\end{tikzcd}
\end{equation}

Let us now assume again to have a linear exponential pseudocomonad $(\bang, \dig, \der)$ on $\catK$. As an instance of \cref{thm:seely-equivalences-monoidal}, the underlying pseudofunctor of the linear exponential pseudocomonad
acquires the structure of a sylleptic strong monoidal functor $\bang (-) \co (\catK, \oplus, 0) \to (\catK, \otimes, \unit)$ and the Seely equivalences have the form
\begin{equation}
\label{equ:seely-with-biproducts}
\seel^{2}_{A,B} \co \bang A \otimes \bang B \to \bang (A \oplus B)  \mathrlap{,} \qquad
\seeli \co \unit \to \bang 0 \mathrlap{.}