Categorical models for linear logic with $\otimes$, $1$, $\&$, $\top$, $\oplus$, $0$, and $\multimap$ are typically symmetric monoidal closed categories (for modeling $\otimes$, $1$, and $\multimap$) with products (for modeling $\&$ and $\top$) and coproducts (for modeling $\oplus$ and $0$). Is it harmful to additionally require that such a category has exponentials? Exponentials would model a binary operator $\Rightarrow$ for which proofs of $A \vdash B \Rightarrow C$ correspond to proofs of $A \mathbin\& B \vdash C$. Are there sensible categorical models for linear logic that have exponentials, or does the introduction of exponentials make the structure collapse?



Are exponentials in categorical models of linear logic harmful?
No, it does not make the structure collapse. For example consider the category of small categories $\mathbf{Cat}$ --- it is clearly complete and cocomplete cartesian closed category, and moreover it has another closed monoidal structure induced by the "funny tensor" and linear exponents $\mathbb{C} \multimap \mathbb{D}$ given by the category of functors $\mathbb{C} \rightarrow \mathbb{D}$ together with (unnatural) transformations (i.e. "natural transformations" without "naturality" requirement).


Much more is true. Every (small) monoidal category $\langle \mathbb{V}, \otimes, I\rangle$ fully embeds into complete and cocomplete cartesian closed and monoidal closed category. The embedding is given by the usual Yoneda functor $y \colon \mathbb{V} \rightarrow \mathbf{Set}^{\mathbb{V}^{op}}$ and the monoidal closed structure is inherited via the Day convolution:
$$(F \otimes G)(X) = \int^{A, B \in \mathbb{V}} F(A) \times G(B) \times \hom(X, A \otimes B)$$
$$(F \overset{L}\multimap G)(X) = \int\_{A, B \in \mathbb{V}} G(A)^{F(B) \times \hom(A, X \otimes B)}$$
$$(F \overset{R}\multimap G)(X) = \int\_{A, B \in \mathbb{V}} G(A)^{F(B) \times \hom(A, B \otimes X)}$$
where $\overset{L}\multimap$ is the left linear exponent and $\overset{R}\multimap$ is the right linear exponent (which are isomorphic precisely when the tensor $\otimes$ in $\mathbb{V}$ is symmetric).
Moreover, it is easy to verify that Yoneda functor preserves the monoidal closed structures. Therefore, in some sense, every monoidal category can be (co)completed to a cartesian closed category with coproducts. 


