Linear Exponential Comonads without Symmetry

TL;DR

This paper extends the concept of linear exponential comonads from symmetric to general monoidal categories, broadening the theoretical framework for modeling exponential modalities in linear logic.

Contribution

It introduces linear exponential comonads on non-symmetric monoidal categories and establishes foundational results for their properties.

Findings

Extended linear exponential comonads to non-symmetric monoidal categories

Established basic properties of these comonads

Broadened the theoretical framework for linear logic modeling

Abstract

The notion of linear exponential comonads on symmetric monoidal categories has been used for modelling the exponential modality of linear logic. In this paper we introduce linear exponential comonads on general (possibly non-symmetric) monoidal categories, and show some basic results on them.

Equations

$$\!\!\!\!\!\!\!\!\begin{array}[]{rcl}(A,\alpha:A\rightarrow!A)\times(B,\beta:B\rightarrow!B)&=&(A\otimes B,A\otimes B\stackrel{{\scriptstyle\alpha\otimes\beta}}{{\longrightarrow}}!A\otimes!B\stackrel{{\scriptstyle m_{A,B}}}{{\longrightarrow}}!(A\otimes B))\\ 1&=&(I,I\stackrel{{\scriptstyle m_{I}}}{{\longrightarrow}}!I)\end{array}$$

$$(A,\alpha )\otimes (B,\beta )=(A\otimes B,A\otimes B\stackrel{\alpha \otimes \beta }{⟶}!A\otimes !B\stackrel{m_{A,B}}{⟶}!(A\otimes B)).$$

$$\dgARROWLENGTH=4em\begin{diagram}$$

$$!X\otimes !Y⊢!Y\otimes !X\text{lx@proof@logical@and}!X\otimes !Y⊢!(!X\otimes !Y)!X,!Y⊢!(!X\otimes !Y)!X,!Y⊢!X\otimes !Y\text{lx@proof@logical@and}!X⊢!X!Y⊢!Y!(!X\otimes !Y)⊢!Y\otimes !X!(!X\otimes !Y),!(!X\otimes !Y)⊢!Y\otimes !X\text{lx@proof@logical@and}!(!X\otimes !Y)⊢!Y!X\otimes !Y⊢!Y!X,!Y⊢!Y!Y⊢!Y!(!X\otimes !Y)⊢!Y!X\otimes !Y⊢!X!X,!Y⊢!X!X⊢!X$$

$$\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\begin{diagram}$$

$$\begin{diagram}$$

$$\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\begin{diagram}$$

$$\Delta X\otimes \Delta Y=!X\otimes !X\otimes !Y\otimes !Y\stackrel{id\otimes \sigma \otimes id}{⟶}!X\otimes !Y\otimes !X\otimes !Y\stackrel{m\otimes m}{⟶}!(X\otimes Y)\otimes !(X\otimes Y)=\Delta (X\otimes Y).$$

$$\begin{array}[]{rcl}I&=&\{*\}~{}\mbox{with}~{}\|*\|=e\\ A\otimes B&=&A\times B~{}\mbox{with}~{}\|(a,b)\|=\|a\|\cdot\|b\|\\ B\rotatebox[origin={c}]{180.0}{\,$\multimap$\,}A&=&\{(x,f)~{}|~{}x\in M,f:A\rightarrow B~{}\mbox{s.t.}~{}\|f(a)\|=x\cdot\|a\|~{}\mbox{for}~{}a\in A\}~{}\mbox{with}~{}\|(x,f)\|=x\\ A\multimap B&=&\{(x,f)~{}|~{}x\in M,f:A\rightarrow B~{}\mbox{s.t.}~{}\|f(a)\|=\|a\|\cdot x~{}\mbox{for}~{}a\in A\}~{}\mbox{with}~{}\|(x,f)\|=x\\ \end{array}$$

$$\mathbf{Set}^{\mathcal{X}^{\mathit{op}}}\begin{array}[]{c}\mbox{\footnotesize$\mathbf{Lan}_{F^{\mathit{op}}}(\_)$}\\ \longrightarrow\\ \mbox{\tiny$\bot$}\\ \longleftarrow\\ \mbox{\footnotesize$(\_)\circ F^{\mathit{op}}$}\end{array}\mathbf{Set}^{\mathcal{C}^{\mathit{op}}}$$

$$\{((x,y),(|x|\cdot y,x)|x\in X,y\in Y\}:(X,\cdot ,|\_|)\otimes (Y,\cdot ,|\_|)\to (Y,\cdot ,|\_|)\otimes (X,\cdot ,|\_|).$$

$$c_{!Y,!X}\circ ({\epsilon }_Y\otimes {\epsilon }_X)\circ (!(e_X\otimes id)\otimes !(id\otimes e_Y))\circ d_{!X\otimes !Y}\circ m_{!X,!Y}\circ ({\delta }_X\otimes {\delta }_Y)=i{d}_{!X\otimes !Y}$$

$$\dgARROWLENGTH=1.3em\begin{diagram}$$

$$({\epsilon }_Y\otimes {\epsilon }_X)\circ (!(e_X\otimes id)\otimes !(id\otimes e_Y))\circ d_{!X\otimes !Y}\circ m_{!X,!Y}\circ ({\delta }_X\otimes {\delta }_Y)=c_{!Y,!X}^{-1}=c_{!X,!Y}.\square$$

Full text

1 Introduction

There are two major approaches to the categorical models of the exponential modality $!$ of linear logic [13]. The first is as a comonad which respects the symmetric monoidal structure (the multiplicative conjunction) and creates commutative comonoids (for modelling weakening and contraction). Since the pioneering work of Seely [26] and Lafont [21], this direction was extensively studied by Benton, Bierman, de Paiva and Hyland [7], and now there is a well-accepted notion of linear exponential comonads [8, 18]. Another one, led by Benton [6] and independently by Barber and Plotkin [4], is as an adjunction between a cartesian category (modelling non-linear proofs) and symmetric monoidal category (modelling linear proofs) which respects the cartesian structure and symmetric monoidal structure. Such a situation is neatly captured as a symmetric monoidal adjunction between a cartesian category and a symmetric monoidal category. These two approaches are in harmony: any linear exponential comonad on a symmetric monoidal category gives rise to a symmetric monoidal adjunction between a cartesian category (of coalgebras) and the symmetric monoidal category, while a symmetric monoidal adjunction between a cartesian category and symmetric monoidal category induces a linear exponential comonad on the symmetric monoidal category. See [25] for a compact survey of these results, and for [24] more detaied accounts and proofs.

In this paper we consider a generalization of these categorical axiomatics for exponential modality to the non-symmetric setting, i.e., on monoidal categories which may not be symmetric. This work is motivated by the desire that we should have a uniform way of modelling exponential modality in symmetric/non-symmetric/braided monoidal categories (cf. the authors’ ad hoc treatment of the braided case via braided monoidal comonads [17]), while we also hope that this work leads to a better understanding of modalities in non-commutative (linear) logics [2, 10, 3] in general. For the approach based on adjunctions, the answer seems more or less obvious: replace symmetric monoidal categories by monoidal categories, and symmetric monoidal adjunctions by monoidal adjunctions. The corresponding axiomatics in terms of comonads is more difficult, as the definition of linear exponential comonads heavily replies on the presence of symmetry. Nevertheless, we do give an appropriate notion of linear exponential comonads without symmetry, which however involves a number of non-trivial coherence axioms. We show that our generalization enjoys a good correspondence with the axiomatics based on monoidal adjunctions. After providing a few typical examples which motivate this research, we conclude this paper with some issues for future research.

2 Linear exponential comonads with symmetry

Let us recall the notion of linear exponential comonads on symmetric monoidal categories — for emphasizing the presence of symmetry, below we will call them symmetric linear exponential comonads.

Remark 1

We assume that the reader is familar with the notions of monoidal categories, monoidal functors, monoidal natural transformations, monoidal comonads as well as monoidal adjunctions [12, 20]. A detailed explanation of these concepts aimed at the computer science/logic audience can be found in [24]. Note that, in this paper, by a monoidal functor we mean a lax monoidal functor, thus a functor $F$ equipped with possibly non-invertible coherent arrow $m_{I}:I\rightarrow FI$ and natural transformation $m_{X,Y}:FX\otimes FY\rightarrow F(X\otimes Y)$; when they are invertible, $F$ is said to be strong monoidal.

Definition 1

[8, 18]** Let $\mathcal{C}$ be a symmetric monoidal category. A symmetric linear exponential comonad on $\mathcal{C}$ is a symmetric monoidal comonad $(!:\mathcal{C}\rightarrow\mathcal{C},\delta_{X}:!X\rightarrow!!X,\varepsilon_{X}:!X\rightarrow X,m_{X,Y}:!X\otimes!Y\rightarrow!(X\otimes Y),m_{I}:I\rightarrow!I)$ on $\mathcal{C}$ equipped with monoidal natural transformations $d_{X}:!X\rightarrow!X\otimes!X$ and $e_{X}:I\rightarrow!X$ such that

• •

$(!X,d_{X},e_{X})$* forms a commutative comonoid,*

• •

$d_{X}$* is a coalgebra morphism from $(!X,\delta_{X})$ to $(!X\otimes!X,m_{!X,!X}\circ(\delta_{X}\otimes\delta_{X}))$,*

• •

$e_{X}$* is a coalgebra morphisms from $(!X,\delta_{X})$ to $(I,m_{I})$, and*

• •

$\delta_{X}$* is a comonoid morphism from $(!X,d_{X},e_{X})$ to $(!!X,d_{!X},e_{!X})$*

for each $X$.

Theorem 1

Any symmetric monoidal adjunction \mathcal{X}\begin{array}[]{c}\mbox{\footnotesizeF}\\ \longrightarrow\\ \mbox{\tiny\bot}\\ \longleftarrow\\ \mbox{\footnotesizeU}\end{array}\mathcal{C} between a cartesian category $\mathcal{X}$ and a symmetric monoidal category $\mathcal{C}$ gives rise to a symmetric linear exponential comonad $FU$ on $\mathcal{C}$.

Proof. Follows from routine calculation. $\square$

Theorem 2

Given a symmetric linear exponential comonad $!$ on a symmetric monoidal category $\mathcal{C}$, its category of Eilenberg-Moore coalgebras $\mathcal{C}^{!}$ is a cartesian category, with

[TABLE]

Moreover, the comonadic adjunction \mathcal{C}^{!}\begin{array}[]{c}\longrightarrow\\ \mbox{\tiny\bot}\\ \longleftarrow\end{array}\mathcal{C} is symmetric monoidal with respect to the cartesian products of $\mathcal{C}^{!}$ and monoidal products of $\mathcal{C}$.

Proof. A detailed and accessible proof can be found in [24]. Here we shall sketch its outline. Since $!$ is a symmetric monoidal comonad, the category of coalgebras $\mathcal{C}^{!}$ is symmetric monoidal with $I=(I,m_{I})$ and

[TABLE]

Then we can show that $d_{X}$ and $e_{X}$ form a comonoid on the cofree coalgebra $(!X,\delta_{X}:!X\rightarrow!!X)$ in $\mathcal{C}^{!}$. Moreover, they induce a comonoid on any coalgebra $(A,\alpha)$ via the retraction $\alpha:A\rightarrow!A$ and $\varepsilon_{A}:!A\rightarrow A$. The induced comonoid structure on each coalgebra extends to natural transformations $d_{(A,\alpha)}:(A,\alpha)\rightarrow(A,\alpha)\otimes(A,\alpha)$ and $e_{(A,\alpha)}:(A,\alpha)\rightarrow(I,m_{I})$. Finally we can appeal to the folklore result that any symmetric monoidal category with a natural comonoid structure on every object is a cartesian category. The comonadic adjunction is symmetric monoidal because its left adjoint is a strong symmetric monoidal functor [20]. $\square$

Symmetry appears in many places in the definition of symmetric linear exponential comonads as well as the proof of Theorem 2 (sometimes rather implicitly, for instance for making $X\mapsto!X\otimes!X$ a monoidal functor). However, note that, only the symmetry of the form $!X\otimes!Y\rightarrow!Y\otimes!X$ is needed in the proof. Moreover, such a symmetry $!X\otimes!Y\rightarrow!Y\otimes!X$ can be re-defined from other constructs:

Proposition 1

In a symmetric monoidal category with a symmetric linear exponential comonad, the morphism

[TABLE]

agrees with the symmetry $!X\otimes!Y\rightarrow!Y\otimes!X$.

A proof is given in Appendix A. This observation suggests that it should be possible to define a linear exponential comonad without assuming symmetry (i.e. on any monoidal category), by using this re-defined “symmetry”, so that its category of coalgebras is cartesian and the induced comonadic adjunction becomes monoidal. In the next section, we give such a definition of linear exponential comonads on monoidal categories.

Remark 2

A proof corresponding to this re-defined “symmetry” in multiplicative linear logic would be:

[TABLE]

It is not possible to remove the cut in this proof in the non-commutative setting, unless we assume the exchange rule on $!$-formulas. Thus our choice of taking this derived “symmetry” as a basic notion, while makes a good sense at the semantic level, does not lead to a pleasant proof system (with the cut-elimination property) at the syntactic level.

3 Linear exponential comonads without symmetry

Definition 2

A linear exponential comonad on a monoidal category $\mathcal{C}$ is a monoidal comonad$(!,\delta,\varepsilon,m,m_{I})$ on $\mathcal{C}$ equipped with a monoidal natural transformation $e_{X}:!X\rightarrow I$ and a natural transformation $d_{X}:!X\rightarrow!X\otimes\,!X$ such that, with $\sigma_{X,Y}=(\varepsilon_{!Y}\otimes\varepsilon_{!X})\circ(!(e_{X}\otimes id)\otimes\,!(id\otimes e_{Y}))\circ d_{!X\otimes\,!Y}\circ m_{!X,!Y}\circ(\delta_{X}\otimes\delta_{Y}):!X\otimes!Y\rightarrow!Y\otimes!X$,

1. (1)

the following diagram commutes:

[TABLE] 2. (2)

$m_{!Y,!X}\circ\sigma_{!X,!Y}=!\sigma_{X,Y}\circ m_{!X,!Y}$, 3. (3)

$\sigma^{-1}_{X,Y}=\sigma_{Y,X}$, 4. (4)

the following diagram commutes:

[TABLE] 5. (5)

*the following diagrams commute,

\dgARROWLENGTH=1.5em*

[TABLE] 6. (6)

$(!X,e_{X},d_{X})$* is a comonoid in $\mathcal{C}$,* 7. (7)

$e_{X}$* and $d_{X}$ are coalgebra morphisms, and* 8. (8)

$\delta_{X}$* is a comonoid morphism.*

Remark 3

In this definition, the conditions (1)-(5) involve $\sigma$. Other conditions are independent of $\sigma$, and are actually the same as the conditions for the symmetric linear exponential comonads.

Theorem 3

Any monoidal adjunction \mathcal{X}\begin{array}[]{c}\mbox{\footnotesizeF}\\ \longrightarrow\\ \mbox{\tiny\bot}\\ \longleftarrow\\ \mbox{\footnotesizeU}\end{array}\mathcal{C} between a cartesian category $\mathcal{X}$ and a monoidal category $\mathcal{C}$ gives rise to a linear exponential comonad $FU$ on $\mathcal{C}$.

Proof: Follows from routine calculation. $\square$

Theorem 4

Given a linear exponential comonad $!$ on a monoidal category $\mathcal{C}$, its category of coalgebras $\mathcal{C}^{!}$ is cartesian. The comonadic adjunction between $\mathcal{C}^{!}$ and $\mathcal{C}$ is monoidal.

Proof: The proof is analogous to the symmetric case, with some extra care on the use of $\sigma$ instead of symmetry. (In fact, our conditions on linear exponential comonads are chosen so that the proof can mimick the symmetric case.) The condition (1) implies that the functor $\Delta X=!X\otimes\,!X$ is monoidal with $I\stackrel{{\scriptstyle m_{I}\otimes m_{I}}}{{\longrightarrow}}!I\otimes\,!I=\Delta(I)$ and

[TABLE]

The condition (2) is for making ! “symmetric monoidal” with respect to $\sigma$. The conditions (3) and (4) imply that $\sigma$ behaves like a symmetry. The condition (5) implies that $d$ is a monoidal natural transformation from $!$ to $\Delta$ defined as above. The condition (6), together with the fact that the (co-)commutativity $\sigma_{X,X}\circ d_{X}=d_{X}$ is derivable from other axioms, says that $(!X,d_{X},e_{X})$ is a “commutative” comonoid. Then we are able to mimick the proof for the case with symmetry. First, we can show that $\mathcal{C}^{!}$ is symmetric monoidal — $\sigma$ extends to a symmetry on $\mathcal{C}^{!}$. Second, we have that $d_{X}$ and $e_{X}$ from a comonoid on the cofree coalgebra on $X$, which naturally extends to all coalgebras. Thus $\mathcal{C}^{!}$ is a symmetric monoidal category with a natural comonoid structure on all objects. $\square$

A symmetric linear exponential comonad can be characterized as a symmetric monoidal comonad such that the induced symmetric monoidal structure on the category of coalgebras is cartesian [23]. As a corollary to the theorems above, this characterization extends to the non-symmetric case, just by dropping all “symmetric”:

Theorem 5

A monoidal comonad is a linear exponential comonad if and only if the induced monoidal structure on the category of coalgebras is cartesian.

The following results, which are standard in the symmetric case, easily follow from the theorems above.

Proposition 2

In a monoidal category $\mathcal{C}$ with a linear exponential comonad $!$ and finite products, there is a natural isomorphism $!X\otimes!Y\cong!(X\times Y)$ as well as an isomorphism $I\cong!1$ making $!$ a strong monoidal functor from $(\mathcal{C},\times,1)$ to $(\mathcal{C},\otimes,I)$.

Proposition 3

Suppose that $\mathcal{C}$ is a monoidal (left or right) closed category with a linear exponential comonad $!$. Then there exists a cartesian closed category $\mathcal{X}$ and a monoidal adjunction \mathcal{X}\begin{array}[]{c}\mbox{\footnotesizeF}\\ \longrightarrow\\ \mbox{\tiny\bot}\\ \longleftarrow\\ \mbox{\footnotesizeU}\end{array}\mathcal{C} such that $!$ agrees with the induced comonad $FU$. In addition, if $\mathcal{C}$ has finite products, the co-Kleisli category $\mathcal{C}_{!}$ is cartesian closed, and the co-Kleisli adjunction is monoidal.

Note that, in a monoidal bi-closed category (with $X\otimes(\_)\dashv X\multimap(\_)$ and (\_)\otimes X\dashv(\_)\rotatebox[origin={c}]{180.0}{\,\multimap\,}X) with a linear exponential comonad $!$, $!X\multimap Y$ may not be isomorphic to Y\rotatebox[origin={c}]{180.0}{\,\multimap\,}!X, but they are isomorphic in the co-Kleisli category.

4 Examples

Obviously, symmetric linear exponential comonads are instances of our linear exponential comonads:

Proposition 4

A linear exponential comonad on a symmetric monoidal category is a symmetric linear exponential comonad if and only if $\sigma$ (given in Definition 2) agrees with the symmetry.

Here is a simple example of a non-symmetric monoidal bi-closed category with a linear exponential comonad.

Example 1

Let $M=(M,\cdot,e)$ be a (non-commutative) monoid and consider the slice category $\mathbf{Set}/M$. Thus an object of $\mathbf{Set}/M$ is a set $A$ equipped with an $M$-valued map $\|\_\|_{A}:A\rightarrow M$ (often the subscript will be omitted), and a morphism $f:(A,\|\_\|_{A})\rightarrow(B,\|\_\|_{B})$ in $\mathbf{Set}/M$ is a map $f:A\rightarrow B$ such that $\|f(a)\|=\|a\|$ holds for any $a\in A$. $\mathbf{Set}/M$ is monoidal bi-closed with

[TABLE]

There is a linear exponential comonad $!$ on $\mathbf{Set}/M$ given by $!A=\{a\in A~{}|~{}\|a\|=e\}$ with $\|a\|=e$, whose category of coalgebras is equivalent to $\mathbf{Set}$.

Presheaves are a rich source of examples:

Example 2

Let $F:\mathcal{X}\rightarrow\mathcal{C}$ be a strong monoidal functor from a cartesian category $\mathcal{X}$ to a monoidal category $\mathcal{C}$. The left Kan extension along $F^{\mathit{op}}:\mathcal{X}^{\mathit{op}}\rightarrow\mathcal{C}^{\mathit{op}}$ gives a monoidal adjunction

[TABLE]

between the cartesian closed category $\mathbf{Set}^{\mathcal{X}^{\mathit{op}}}$ and the monoidal bi-closed category $\mathbf{Set}^{\mathcal{C}^{\mathit{op}}}$ (with the monoidal structure on $\mathbf{Set}^{\mathcal{C}^{\mathit{op}}}$ given by Day’s tensor product [11]). From this we obtain a linear exponential comonad $!$ on $\mathbf{Set}^{\mathcal{C}^{\mathit{op}}}$ where $\displaystyle!G=\mathbf{Lan}_{F^{\mathit{op}}}(G\circ F^{\mathit{op}})=\int^{X\in\mathcal{X}}\mathcal{C}(\_,FX)\times G(FX)$ for $G:\mathcal{C}^{\mathit{op}}\rightarrow\mathbf{Set}$.

Remark 4

The two examples above can be extended to more involved ones using categorical glueing (given by comma categories, or more generally change-of-base of monoidal closed bi-fibrations along monoidal functors). Such glueing constructions are known for the symmetric cases [15, 14, 18], and can be generalized to the non-symmetric cases without much difficulty.

We conclude this section with an example with non-symmetric braiding [19] taken from our previous work [17].

Example 3

Let $G$ be a group with the unit element $e$. A crossed $G$-set is a set $X$ equipped with a group action $\cdot:G\times X\rightarrow X$ and a map $|\_|:X\rightarrow G$ such that, for any $g\in G$ and $x\in X$, $|g\cdot x|=g|x|g^{-1}$ holds. Now let $\mathbf{XRel}(G)$ be the category whose objects are crossed $G$-sets, and a morphism from $(X,\cdot,|\_|)$ to $(Y,\cdot,|\_|)$ is a binary relation $r:X\rightarrow Y$ such that $(x,y)\in r$ implies $(g\cdot x,g\cdot y)\in r$ as well as $|x|=|y|$. The composition and identity are just those of binary relations. $\mathbf{XRel}(G)$ is monoidal, with $(X,\cdot,|\_|)\otimes(Y,\cdot,|\_|)=(X\times Y,(g,(x,y))\mapsto(g\cdot x,g\cdot y),(x,y)\mapsto|x||y|)$. This monoidal structure is not symmetric but braided: the braiding on $(X,\cdot,|\_|)$ and $(Y,\cdot,|\_|)$ is given by

[TABLE]

(In fact, $\mathbf{XRel}(G)$ forms a ribbon category [27, 28], thus allows interpretation of tangles [17].) There is a linear exponential comonad on $\mathbf{XRel}(G)$ which sends $(X,\cdot,|\_|)$ to the finite multiset of $\{x\in X~{}|~{}|x|=e\}/\sim$ (where $x\sim y$ if $g\cdot x=y$ for some $g\in G$) with trivial action $g\cdot u=u$ and valuation $|u|=e$.

Note that linear exponential comonads on braided monoidal categories in [17] are the linear exponential comonads in this paper such that $\sigma$ agrees with the braiding, thus the situation is exactly the parallel of the symmetric case.

5 Conclusion and future work

We have given the notion of linear exponential comonads on arbitrary monoidal categories, and shown that it has a good correspondence to the axiomatics based on monoidal adjunctions. There are a number of immediate issues which are left as the future work:

Simpler axiomatization

Unfortunately, our definition of linear exponential comonads involve a number of coherence axioms which are rather hard to be used in practice. We do expect that some of the axioms are actually redundant, and some (conceptually or technically) simpler axiomatization can be found. As an easy direction, it would be interesting to consider the case with finite products (additive products) which would allow some substantially simpler axiomatics where the key isomorphism $\sigma_{X,Y}:!X\otimes!Y\rightarrow!Y\otimes!X$ can be simply given by $!X\otimes!Y\cong!(X\times Y)\cong!(Y\times X)\cong!Y\otimes!X$.

Proof systems and term calculi

The absence of symmetry causes a number of troubles at the level of syntax, i.e., on proof systems or term calculi (linear lambda calculi). From the proof theoretical point of view, the nasty issue on cut-elimination must be remedied by introducing Exchange rules for $!$-types, whose precise formulation can be of some interest. As a direction closer to the categorical models, it would be nice if we have a (equationally) sound and complete term calculus for monoidal bi-closed categories with a linear exponential comonad, like the DILL calculus [4] for the symmetric case. The case of (non-symmetric) $*$-autonomous categories [5, 9] with a linear exponential comonad should be also interesting, as there can be a term calculus just with linear/non-linear implications and the falsity type as type constructs [16].

Issues on (2- or bi-)categories of models

While linear exponential comonads and monoidal adjunctions are closely related, the (2- or bi-)categories of these structures are not (bi-)equivalent. We believe that the situation is the same as the symmetric case [22, 25], but the precise details (the correct formulation of morphisms in particular) are yet to be examined.

Non-monoidal exponential modality

The exponential modality of the non-commutative propositional linear logic in [10] does not satisfy the monoidality $!X\otimes!Y\rightarrow!(X\otimes Y)$ (hence promotion is not valid in general); some justification for not allowing promotion/monoidality is given in ibid. Clearly our linear exponential comonads are not appropriate for modelling such a non-monoidal case, while we do not know a suitable categorical axiomatics for the non-monoidal exponential modality.

Acknowledgements

I thank Shin-ya Katsumata for helpful discussions, and Kazushige Terui for his advice on non-commutative linear logic and cut-elimination. This research is partly supported by the Grant-in-Aid for Scientific Research (C) 15K00013.

Appendix A Proof of Proposition 1

Let $c$ be the symmetry. The following commutative diagram shows that

[TABLE]

holds.

[TABLE]

[TABLE]

From this, we have

[TABLE]