We show the doctrine of $\ast$-autonomous categories is “2-conservative” over the doctrine of closed symmetric monoidal categories, i.e. the universal map from a closed symmetric monoidal category to the $\ast$-autonomous category that it freely generates is fully faithful.
This implies that linear logics and graphical calculi for $\ast$-autonomous categories can also be interpreted canonically in closed symmetric monoidal categories.

In particular, our result implies that every closed symmetric monoidal category can be fully embedded in a $\ast$-autonomous category, preserving both tensor products and internal-homs.
But in fact we prove this directly first with a Yoneda-style embedding (an enhanced “Hyland envelope” that can be regarded as a polycategorical form of Day convolution), and deduce 2-conservativity afterwards from double gluing and a technique of Lafont.

Since our method uses polycategories, it also applies to other fragments of $\ast$-autonomous structure, such as linear distributivity.
It can also be enhanced to preserve any desired family of nonempty limits and colimits.

§ INTRODUCTION

Duality in monoidal categories is useful for many purposes.
For instance, if $A$ has a dual $\d A$, then the internal-hom $A\hom B$ is isomorphic to $\d A \ten B$.
Thus, graphical calculi for compact closed categories (where all objects have duals) allow strings to be simply bent around to represent duals, whereas it appears that additional “clasps” and “bubbles” (as in [6]) are needed for general internal-homs.

Unfortunately, a symmetric monoidal category cannot be fully embedded in a compact closed one unless it is traced [20].
But a weaker notion of duality is that of a $\ast$-autonomous category [1], where instead $A\hom B$ is isomorphic to $\d{(A \ten \d B)}$.
Here no traces are induced, and indeed every closed symmetric monoidal category with pullbacks can be embedded in a $\ast$-autonomous category by the Chu construction [7]; but this embedding does not preserve the internal-homs.
Thus, it is natural to ask whether any closed symmetric monoidal category can be fully embedded in a $\ast$-autonomous category preserving the closed structure.

We will show the answer is yes, using a more refined Chu construction.
The problem with the ordinary Chu construction on is that there is no canonical dualizing object $\bot$, and in particular none for which all objects of are reflexive (i.e. $A \cong (A\hom \bot)\hom \bot$).
Now in Isbell duality [18], the hom-functor $\cC(-,-)$ is a canonical “dualizing object” between presheaf and co-presheaf categories, for which all representables are reflexive.
But to apply the Chu construction, we need the dualizing object to live in the same category as the representables themselves.

The modules of [17] achieve this for polycategories, with a resulting Chu construction called the envelope.
We modify Hyland's envelope so that the embedding preserves any desired tensor and cotensor products, by adapting the standard trick [13, 21] for making Yoneda embeddings preserve colimits.
We then deduce the result by representing closed symmetric monoidal categories by certain polycategories.

The existence of such an embedding establishes that there is some way to interpret $\ast$-autonomous graphical calculi in closed symmetric monoidal categories.
But if we only know that there exists such an embedding, then it could be that the interpretation of a string diagram in some closed symmetric monoidal category might depend on the embedding chosen.
We can remedy this by proving that the universal map from a closed symmetric monoidal category to a $\ast$-autonomous category (the unit of a free-forgetful adjunction) is fully faithful, for then the interpretation obtained from this universal embedding will necessarily coincide with the interpretation obtained from some other embedding.
I do not know a standard name for the full-faithfulness of such a universal map; I will call it 2-conservativity of the doctrine of $\ast$-autonomous categories over that of closed symmetric monoidal categories (another name sometimes used is “abstract full completeness”).

The $\ast$-autonomous category freely generated by a closed symmetric monoidal category is not very explicit.
But fortunately, Lafont [24] already described a general technique for enhancing Yoneda-type embedding theorems to 2-conservativity results, using Artin gluing (the semantic form of logical relations).
In our case we we need a slightly enhanced form of “double gluing” [31, 15, 14], but otherwise essentially the same technique works.[It is claimed in [15, 14] that this can be proven using double gluing with an ordinary Yoneda embedding, but this doesn't appear to be true; see <ref>.]

It follows that we can use circuit diagrams for $\ast$-autonomous categories [2], or term calculi for linear logic (e.g. [26, 27]), to reason about closed symmetric monoidal categories, giving a new perspective on why the same “Kelly-MacLane graphs” (and enhanced versions incorporating units) appear in coherence for closed symmetric monoidal categories and for $\ast$-autonomous categories [23, 32, 4, 5, 16].
We also obtain a semantic proof of the conservativity of multiplicative linear logic over its intuitionistic variant.

Throughout the paper, we use multicategories and polycategories systematically,
obtaining cleaner and more general proofs and constructions.
For instance, polycategorical Chu constructions and double gluing, and their $\ast$-autonomous operations, are characterized by universal properties.
Our embedding theorem also applies to more general polycategories, yielding 2-conservativity of $\ast$-autonomous categories over other structures such as linearly distributive categories (this was proven by cut-elimination in [2]).
We can also make the embedding preserve any desired polycategorical limits and colimits, although only nonempty limits and colimits in a closed symmetric monoidal categories are polycategorical; this gives a semantic explanation for why only the inclusion of an initial object $\mathbf{0}$ breaks the conservativity of classical multiplicative-additive linear logic over its intuitionistic version [28].

Thanks to Sam Staton, Kirk Sturtz, and Todd Trimble for useful conversations.

§ ADDING DUALS TO POLYCATEGORIES

Recall that a multicategory is like a category but permits the source of a morphism to be an arbitrary finite list of objects; if $\Gamma$ is such a list we write $f:\Gamma\to B$ or $f\in \cC(\Gamma;B)$.
All our multicategories will be symmetric (include actions by permutations of $\Gamma$), so we henceforth drop this adjective.
A closed symmetric monoidal category $(\cC,\ten,\unit,\hom)$ can be regarded as a multicategory that is representable and closed, meaning there are objects with universal properties:

\begin{gather*}
% \cC(A_1,\dots,A_n;B) &= \cC(A_1\ten\cdots\ten A_n,B)
\cC(\Gamma;C) \cong \cC(\Gamma,\unit;C)\qquad
\cC(\Gamma,A,B;C) \cong \cC(\Gamma,A\ten B; C)\\
\cC(\Gamma,A;B) \cong \cC(\Gamma; A\hom B).
\end{gather*}

Similarly, an (always symmetric) polycategory[A.k.a. “colored dioperad”] [30] allows both source and target to be arbitrary lists of objects, though (unlike in other structures such as PROPs) composition is restricted to occur along one object at a time, e.g.
\[\cP(\Gamma,A;\Delta) \times \cP(\Sigma;\Pi,A) \to \cP(\Gamma,\Sigma;\Delta,\Pi). \]

Note that a multicategory is just a polycategory that is co-unary, i.e. all codomains have one object.

A $\ast$-autonomous category can be regarded as a representable[Note that a representable multicategory is not representable as a co-unary polycategory.] polycategory with duals, i.e. having objects with universal properties:

\begin{gather*}%{2}
\cE(\Gamma,A,B;\Delta) \cong \cE(\Gamma,A\ten B; \Delta) \qquad
\cE(\Gamma;\Delta,A,B) \cong \cE(\Gamma; \Delta,A\coten B) \\
\cE(\Gamma;\Delta) \cong \cE(\Gamma,\unit;\Delta) \qquad
\cE(\Gamma;\Delta) \cong \cE(\Gamma;\Delta,\bot)\qquad
\cE(\Gamma,A; \Delta) \cong \cE(\Gamma;\Delta,\d A)
\end{gather*}

A $\ast$-polycategory [17] is a polycategory with specified strictly involutive duals ($\dd{A} = A$).
In particular, a representable $\ast$-polycategory is $\ast$-autonomous.

The forgetful functor from $\ast$-polycategories to polycategories has a left adjoint $\cP\mapsto\fsp\cP$.
The objects of $\fsp\cP$ consist of two copies of the objects of , denoted $A$ and $\Abar$ respectively.
The morphisms are determined by saying that

\[ \fsp\cP(\Gamma,\overline\Pi; \Delta, \overline\Sigma) = \cP(\Gamma,\Sigma; \Delta,\Pi). \]

Composition is inherited from , perhaps in the other order.
For instance, if $f\in \fsp\cP(A,\Bbar;C,\Dbar) = \cP(A,D;C,B)$ and $g\in \fsp\cP(C,\Xbar;\Bbar,Y) = \cP(C,B;\,Y,X)$ then $g\circ^{\fsp\cP}_C f = g\circ_C^\cP f$ and $f \circ_{\d B}^{\fsp\cP} g = g\circ_B^\cP f$.
Thus $\cP$ embeds fully-faithfully in $\fsp\cP$.

Any polycategory functor preserves duals, so if has duals the map $\cP \to \fsp\cP$ is essentially surjective, hence an equivalence.
Thus any $\ast$-autonomous category is equivalent to a representable $\ast$-polycategory.[This was shown by [19] using a right adjoint instead of our left adjoint.  In fact  are both 2-monadic and 2-comonadic over the 2-category of polycategories, functors, and natural isomorphisms, and the 2-monad and 2-comonad are pseudo-idempotent [22].]

Any tensor product $A\ten B$ in is also a tensor product in $\fsp\cP$, while $\overline{(A\ten B)}$ is a cotensor product $\Abar \coten \Bbar$ in $\fsp\cP$.
The situation for cotensor products $A\coten B$ is dual, while that for units and counits is similar.

However, even if has all tensor and/or cotensor products, $\fsp\cP$ will not in general have $\d A \ten B$ or $\d A \coten B$.

If is a multicategory regarded as a co-unary polycategory, then $\fsp\cC(\Gamma,\d\Pi;\Delta,\d\Sigma)$ is nonempty just when $|\Delta\cup\Pi|=1$.
(This left adjoint to the forgetful functor from $\ast$-polycategories to multicategories appears in [12].)
In this case, if is closed, the hom-object $A\hom B$ is a cotensor product $\d A \coten B$ in $\fsp\cC$.
For by definition:

\begin{align*}
\fsp\cC(\Gamma,\overline\Pi; \Delta, \overline\Sigma, A\hom B)
&\cong \cC(\Gamma,\Sigma; \Pi,\Delta, A\hom B)\\
\fsp\cC(\Gamma,\overline\Pi; \Delta, \overline\Sigma, \Abar, B)
&\cong \cC(\Gamma,\Sigma, A ; \Pi,\Delta, B)
\end{align*}

and both right-hand sides are nonempty only if $\Pi = \Delta=\emptyset$, in which case they are naturally isomorphic by the universal property of $A\hom B$ in .
Let $\Umulti$ denote the forgetful functor from polycategories to multicategories; then we have shown:

If is closed symmetric monoidal, there is a $\ast$-polycategory $\fsp\cC$ and a fully faithful functor $\cC \to \Umulti(\fsp\cC)$ that preserves tensor products (including the unit) and takes internal-homs $A\hom B$ to cotensor products $\Abar \coten B$.

Therefore, to embed in a $\ast$-autonomous category preserving both tensor products and internal-homs, it will suffice to embed the $\ast$-polycategory $\fsp\cC$ in a $\ast$-autonomous category preserving those tensor and cotensor products that exist.

§ MODULES

Let be a polycategory.
Following <cit.>, a -module is a family of sets $\cU(\Gamma;\Delta)$ with symmetric group actions and left and right actions by
\begin{align*}
\cP(\Pi;\Sigma,A) \times \cU(A,\Gamma;\Delta) &\to \cU(\Pi,\Gamma;\Sigma,\Delta)\\
\cU(\Gamma;\Delta,A)\times \cP(A,\Pi;\Sigma) &\to \cU(\Gamma,\Pi;\Delta,\Sigma)
\end{align*}

satisfying the same associativity and unit laws as the composition in a polycategory.

* The hom-sets $\cP(\Gamma;\Delta)$ form a -module, which we denote simply .

* For any $\Pi,\Sigma$ and module , we have a shifted module $\cU[\Pi;\Sigma]$ defined by $\cU[\Pi;\Sigma](\Gamma;\Delta) = \cU(\Gamma,\Pi;\Delta,\Sigma)$.

* For an object $A\in \cP$, we have the representable modules at $A$:

\[\yon_A = \cP[\,;A] \qquad\text{and}\qquad \noy{A} = \cP[A;\,]. \]

A module (multi-)morphism $(\cU_1,\dots,\cU_n)\to \cV$ consists of functions

\[ \cU_1(\Gamma_1;\Delta_1) \times \cdots \times \cU_n(\Gamma_n;\Delta_n) \to \cV(\Gamma_1,\dots,\Gamma_n; \Delta_1,\dots,\Delta_n) \]

that commute with the symmetric group actions and the actions of .
(A nullary morphism $()\to \cV$ is just an element of $\cV(\,;\,)$.)
This defines a multicategory $\modp$.

The multicategory $\modp$ is closed and representable.

Let $(\cU \hom \cV)(\Gamma;\Delta)$ be the set of (unary) module morphisms $\cU \to \cV[\Gamma;\Delta]$.
The unit is defined by $\cI(\,;\,) = 1$ and all other sets empty.
The tensor products can be obtained formally by an adjoint functor theorem (since $\modp$ is locally presentable), or constructed more explicitly as in <cit.>.

For an alternative proof of <ref>, let $F_{\ten} \Umulti \fsp \cP$ be the free symmetric strict monoidal category on the underlying multicategory of $\fsp\cP$.
Its objects are finite lists of objects and and their formal duals, but by symmetry each is isomorphic to one of the form $(\Gamma,\overline\Delta)$ where $\Gamma$ and $\Delta$ consist of objects of .
A -module is then equivalent to an ordinary presheaf on $F_{\ten} \Umulti \fsp \cP$ defined by $(\Gamma,\overline\Delta)\mapsto \cU(\Gamma;\Delta)$.
Now since $F_{\ten} \Umulti \fsp \cP$ is symmetric monoidal, its presheaf category has a closed symmetric monoidal Day convolution [10] monoidal structure, which coincides with that described above.

Thus, $\modp$ is a closed symmetric monoidal category.
We regard it as a polycategorical “presheaf category”, as justified by the following Yoneda lemmas:

We have natural isomorphisms

(_A; )    ≅(A; )        (A;)    ≅( ;A)

(Γ,_A ; )    ≅(Γ; [A; ])        (Γ,A ; )    ≅(Γ; [ ;A])

(_A )    ≅[A; ]        (A )    ≅[ ;A]

This follows formally from <ref> and properties of Day convolution, but we can also give an explicit proof.
Since $1_A \in \cP(A;A) = \yon_A(A;\,)$, any $\phi:\yon_A \to \cV$ induces $\phi(1_A) \in \cV(A;\,)$.
Conversely, from $x\in \cV(A;\,)$ we define $\psi_x:\yon_A \to \cV$ by:

\[ \Big(f\in \yon_A(\Gamma;\Delta) = \cP(\Gamma;\Delta,A)\Big)
\mapsto
\Big(x \circ_A f \in \cV(\Gamma;\Delta) \Big).
\]

The associativity of the -action on ensures that this is a -module morphism.
Clearly $\psi_x(1_A) = x \circ_A 1_A = x$, while on the other side we have

\begin{equation*}
\psi_{\phi(1_A)}(f) = \phi(1_A) \circ_A f
= \phi (1_A \circ_A f)
= \phi(f).
\end{equation*}

This, and a dual calculation, proves (<ref>).
For (<ref>), we have

\begin{equation*}
% \begin{alignat*}{2}
(\yon_A \hom \cV)(\Gamma;\Delta)
= \modp(\yon_A, \cV[\Gamma;\Delta])\\
\cong
\cV[\Gamma;\Delta](A;\,)  % &\qquad \text{(by~\ref{item:yoneda1})}\\
\cV(A,\Gamma;\Delta)
\cong \cV[A;\,](\Gamma;\Delta)
% \end{alignat*}
\end{equation*}

and dually.
Finally, (<ref>) follows from (<ref>) and the universal property of $\hom$.

$(\yon_A \hom \cP) \cong \noy{A}$ and $(\noy{A}\hom \cP) \cong \yon_A$.

In particular, both kinds of representable are reflexive: $\yon_A \cong ((\yon_A \hom \cP)\hom\cP)$ and $\noy A \cong ((\noy A \hom \cP)\hom\cP)$.

There are full embeddings of multicategories

\[\yon : \Umulti(\cP)\to\modp \qquad\text{and}\qquad \noy{} : \Umulti(\cP\op) \to \modp.\]

From <ref>, we have

\begin{align*}
\modp(\yon_{A_1},\dots,\yon_{A_n};\yon_B) &\cong \yon_B(A_1,\dots,A_n;\,) = \cP(A_1,\dots,A_n;B)\\
\modp(\noy{A_1},\dots,\noy{A_n};\noy B) &\cong \noy B(\,;A_1,\dots,A_n) = \cP(B;A_1,\dots,A_n).
\end{align*}

Functoriality is easy to check.

§ THE POLYCATEGORICAL CHU CONSTRUCTION

Let be a multicategory; a presheaf on can be defined equivalently as either:

* A module (as in <ref>) over qua co-unary polycategory, whose only nonempty values have the form $\cU(\Gamma;\,)$.

* An ordinary presheaf on the free symmetric strict monoidal category $F_{\ten}\cE$ generated by .

* An extension of to a co-subunary polycategory, i.e. one in which all morphisms have codomain arity 0 or 1.

* Explicitly as in <cit.>; here we consider only set-valued presheaves.

When is a presheaf on , we write $\cE(\Gamma;\bbot)$ for the set $\bbot(\Gamma;\,)$ as in <ref>.
This is not very abusive, since by <ref> it is isomorphic to $\mod{\cE}(\yon_\Gamma;\bbot)$.

The following multicategorical Chu construction first appeared, to my knowledge, in [29], although <cit.> contains a similar construction for bicategories.
It explains the Chu tensor product [7] by a universal property.

The Chu construction $\chu(\cE,\bbot)$
is the following $\ast$-polycategory:

* Its objects are triples $A=(A\p,A\m,\uA)$ where $A\p$ and $A\m$ are objects of , and $\uA \in \cE(A\p,A\m;\bbot)$.
We have $\d{(A\p,A\m,\uA)} = (A\m,A\p,\uA\sigma)$.

* Its morphisms $f:(A_1,\dots,A_m) \to (B_1,\dots,B_n)$ are families of morphisms in :

f_j    : (A_1, …, A_m, B_1, …, B_j,…B_n) ⟶B_j          (1 ≤j ≤n)

f_i    : (A_1, …, A_i,…A_m, B_1, …, B_n) ⟶A_i          (1≤i ≤m)

: (A_1,…,A_m,B_1,…,B_n) ⟶
(where hats indicate omitted entries) such that $\underline{\smash{B_j}}\circ_{B_j\p} f\p_j = \uf$ and $\underline{\smash{A_i}}\circ_{A_i\m} f\m_i = \uf$ (modulo permutations).
If $m=n=0$, the only datum is $\uf : () \to \bbot$.

* The identity of $(A\p,A\m,\uA)$ is $(1_{A\p},1_{A\m},\uA)$; composition is induced from .

If is representable and closed with pullbacks, and $\bbot=\yon_\bot$ is representable, then $\chu(\cE,\bot)$ is representable, hence $\ast$-autonomous.

The usual formulas $\unit = (\unit,\bot,\ell)$ and $A\ten B = (A\p\ten B\p, P, \rho)$ can be verified to have the correct universal properties, where $P$ is the pullback

\[
\begin{tikzcd}[baseline=-7mm]
P \ar[r] \ar[d] \drpullback & A\p \hom B\m \ar[d] \\
B\p \hom A\m \ar[r] & (A\p\ten B\p)\hom \bot.
\end{tikzcd}\qedhere
\]

In addition, the multicategorical Chu construction itself has a simple universal property, which generalizes and strictifies that of [25].
Let denote the category of $\ast$-polycategories, and that of co-subunary polycategories.

$\chu$ is right adjoint to the forgetful functor $\ssU: \spoly \to \supoly$, and the adjunction is comonadic.

The counit $\ssU\chu(\cE) \to \cE$ extracts $A\p$ from $A$, $f_1\p$ from a morphism $f:(A_1,\dots,A_m) \to B_1$, and $\uf$ from a morphism $f:(A_1,\dots,A_n) \to ()$.
The unit $\cP \to \chu(\ssU(\cP))$ sends an object $A$ to $(A,\d A, \ep_A)$, where $\ep_A \in \cP(A,\d A;\,)$ is the duality counit, and a morphism $f\in \cP(\Gamma;\Delta)$ to the family of all its co-subunary duality images.

The coalgebras for the induced comonad are co-subunary $\ast$-polycategories, which by <cit.> are equivalent to ordinary $\ast$-polycategories.

§ ENVELOPES

Let be a polycategory; we now describe Hyland's Yoneda-type embedding.

The envelope of is the Chu construction

\[ \envp=\chu(\modp,\cP).\]

Thus, an object of $\envp$ is two modules , with a module map $(\cU,\cV) \to \cP$.
Since $\modp$ is representable and closed with pullbacks, $\envp$ is , and contains $\modp$ as a symmetric monoidal full subcategory via $\cU \mapsto (\cU, \cU\hom\cP, \mathsf{ev})$.
Hence it also contains $\Umulti(\cP)$ as a full sub-multicategory via $A \mapsto (\yon_A, \noy{A}, \gamma_A)$, where $\gamma_A : (\yon_A, \noy{A}) \to \cP$ is composition in .
In fact, Hyland showed:

The assignment $A\mapsto (\yon_A, \noy{A}, \gamma_A)$ extends to a full embedding of polycategories $\cP \into \envp$.

A morphism $g:(\gamma_{A_1},\dots,\gamma_{A_m}) \to (\gamma_{B_1},\dots,\gamma_{B_n})$ in $\envp$ is a compatible family of morphisms in $\modp$:

g_j :       (_A_1,…,_A_m,B_1,…,B_j,…,B_n)    →_B_j

g_i :       (_A_1,…,_A_i,…,_A_m,B_1,…,B_n)    →A_i

:       (_A_1,…,_A_m,B_1,…,B_n)    →.

By (<ref>), each of these is equivalent to a morphism $(A_1,\dots,A_m) \to (B_1,\dots, B_n)$ in , and the compatibility conditions say exactly that they correspond to the same such morphism.
Functoriality is straightforward to verify.

Thus, any polycategory embeds fully-faithfully in a $\ast$-autonomous category, and indeed in a Chu construction.

An explicit way to extract a morphism in from a morphism $g:(\gamma_{A_1},\dots,\gamma_{A_m}) \to (\gamma_{B_1},\dots,\gamma_{B_n})$ is to evaluate the component

\[ \small \begin{tikzcd} \yon_{A_1}(A_1;) \times \cdots \times \yon_{A_m}(A_m;) \times \noy{B_1}(;B_1)\times\cdots\times \noy{B_n}(;B_n) \to \cP(A_1,\dots,A_m;B_1,\dots,B_n)
\end{tikzcd}
\]

of at the identities $(1_{A_1},\dots,1_{A_m},1_{B_1},\dots,1_{B_n})$.

If is an ordinary category regarded as a unary co-unary polycategory, then the categories $[\cP\op,\fSet]$ and $[\cP,\fSet]$ are equivalent to the categories of modules whose only nonempty values have the form $\cU(A;\,)$ and $\cU(\,;A)$, respectively.
The functor $(-)\hom \cP$ restricts to Isbell conjugation interchanging these two subcategories, and the Hyland envelope contains the Isbell envelope [18].

§ PRESERVING TENSORS AND COTENSORS

Hyland's envelope does not preserve any tensor or cotensor products that exist in ,
but we can modify it to do so along the lines of [13] and <cit.>.

Suppose is equipped with a set of tensor and cotensor products that exist (potentially including the nullary cases of a unit and/or counit), which we call distinguished.
Our intended example is $\cP=\fsp\cC$ from <ref>, with the tensor products and unit coming from , and the cotensor products $(\Abar \coten B) = (A\hom B)$.

A $\pj$-module is a module that respects the distinguished tensor and cotensor products.
E.g. if $(A\ten B) \in \cJ$, the induced maps such as
\( \cU(\Gamma,A\ten B;\Delta) \to \cU(\Gamma,A,B;\Delta)\)
are isomorphisms.

Let $\modpj\subseteq \modp$ consist of the $\pj$-modules.
Of course, is a $\pj$-module, as is any shift of a $\pj$-module; thus $\yon_A,\noy{A}\in \modpj$.

The embedding $\yon : \Umulti(\cP)\to\modpj$ preserves distinguished tensor products.
Dually, the embedding $ \noy{} : \Umulti(\cP\op) \to \modpj$ takes distinguished cotensor products (which are tensor products in $\cP\op$) to tensor products.

Let be a $\pj$-module and $\Gamma$ a list of $\pj$-modules.
Then by (<ref>) and the assumption on we have natural bijections:

\begin{align*}
\modp(\Gamma,\yon_A,\yon_B\mathbin;\cU)
&\cong \modp(\Gamma\mathbin; \cU[A,B;\,])\\
&\cong \modp(\Gamma\mathbin ; \cU[A\ten B;\,])\\
&\cong \modp(\Gamma,\yon_{A\ten B}\mathbin; \cU).
\end{align*}

Thus, $\yon_{A\ten B}$ is a tensor product $\yon_A \ten \yon_B$.

The dual statement is similar.

* $\modpj$ is a reflective subcategory of $\modp$.

* If $\cU\in\modp$ and $\cV\in \modpj$ then $(\cU\hom\cV)\in\modpj$.

* $\modpj$ has a closed symmetric monoidal structure such that the reflector is strong monoidal and the inclusion preserves internal-homs.

$\modpj$ is locally presentable, closed under limits, and accessibly embedded, so <ref> follows from the adjoint functor theorem.

Now by definition

\begin{equation*}
(\cU \hom \cV)(\Gamma;\Delta) = \modp(\cU, \cV[\Gamma;\Delta]),
\end{equation*}

so <ref> follows since $\cV$ is a $\pj$-module.

Finally, <ref> follows formally [11]; the tensor product $\tenj$ of $\modpj$ is the reflection of that of $\modp$.

By the formula for $\cU\ten \cV$ on p28 of [17], any elements $u\in \cU(A;\,)$ and $v\in \cV(B;\,)$ induce an element of $(\cU\ten\cV)(A,B;\,)$, hence of $(\cU\tenj\cV)(A\ten B; \,)$ and thence $(\cU\tenj\cV)(C; \,)$ for any $C\to A\ten B$ in .
Thus we have a map

\[ \cP(C, A\ten B) \times \cU(A;\,) \times \cV(B;\,) \too (\cU\tenj \cV)(C;\,) \]

showing that $\tenj$ is similar to Day convolution [10].

Given $\pj$, its envelope is the Chu construction

\[ \envpj=\chu(\modpj,\cP).\]

$\envpj$ is $\ast$-autonomous, contains as a full sub-polycategory, and the inclusion preserves the distinguished tensor and cotensor products.

Since $\modpj$ is a full sub-multicategory of $\modp$, $\envpj$ is a full sub-polycategory of $\envp$.
Since it contains the image of , which is a full sub-polycategory of $\envp$ by <ref>, the inclusion $\cP \into \envpj$ is also full.

Now the embedding of $\modpj$ in $\envpj$, like that of any monoidal category in its Chu construction, preserves tensor products.
Since the embedding of $\Umulti(\cP)$ in $\modpj$ preserves distinguished tensor products by <ref>, so does the composite $\Umulti(\cP) \into \modpj\into \envpj$.
Dually, the composite embedding
$\Umulti(\cP) \into \modpj\op \into \envpj$ preserves distinguished cotensor products, and by <ref> the two embeddings coincide.

Combining <ref>, we obtain our first new embedding theorem.

Any closed symmetric monoidal category can be fully embedded in a $\ast$-autonomous category by a strong symmetric monoidal closed functor.

By <ref>, embeds fully in the $\ast$-polycategory $\fsp\cC$ preserving tensor products and taking homs $A\hom B$ to cotensor products $\Abar \coten B$.
Let consist of these tensor and cotensor products, and embed $\fsp\cC$ in the $\ast$-autonomous category $\env{(\fsp\cC,\cJ)}$, which by <ref> preserves these tensor and cotensor products.

§ PRESERVING LIMITS AND COLIMITS

By a limit in a polycategory we mean a cone of unary morphisms such that

\[ \cP(\Gamma; \Delta,\lim_i A_i) \to \lim_i \cP(\Gamma;\Delta,A_i) \]

is always an isomorphism.
A colimit is a limit in $\cP\op$.

Note that since limits of modules are pointwise, we have

\[ \yon_{(\lim_i A_i)} \cong \lim_i (\yon_{A_i}) \qquad\text{and}\qquad
\noy{(\colim_i A_i)} \cong \lim_i (\noy{A_i}),
\]

but in $\modp$ or $\modpj$ we can say nothing about $\yon_{(\colim_i A_i)}$ or $\noy{(\lim_i A_i)}$.
Now let $\pj$ be as in <ref>, and a set of distinguished limit and colimit cones in .

We have been ignoring size, but should everywhere be a small polycategory, and should be a small set.
(is automatically small once is.)

A $\pjk$-module is a $\pj$-module that in addition respects the distinguished limits and colimits in , i.e. the map

\[ \cU(\Gamma; \Delta,\lim_i D_i) \to \lim_i \cU(\Gamma;\Delta,D_i) \]

is an isomorphism for all distinguished limit cones, and dually for colimits.

is a $\pjk$-module, as is any shift of a $\pjk$-module; hence so are $\yon_A$ and $\noy{A}$.
Let $\modpjk\subseteq\modp$ consist of the $\pjk$-modules.

* $\modpjk$ is a reflective subcategory of $\modp$.

* If $\cU\in\modp$ and $\cV\in \modpjk$ then $(\cU\hom\cV)\in\modpjk$.

* $\modpjk$ has a closed symmetric monoidal structure such that the reflector is strong monoidal and the inclusion preserves internal-homs.

* The embedding $\yon : \Umulti(\cP) \to \modpjk$ preserves distinguished tensor products.
Dually, the embedding $\noy{} : \Umulti(\cP\op)\to \modpjk$ takes distinguished cotensor products to tensor products.

* The embeddings $\yon$
and $\noy{}$
preserve distinguished limits and colimits.

Parts <ref>–<ref> are just like <ref>.
For <ref>, it remains to show that $\yon$ preserves distinguished colimits and $\noy{}$ preserves distinguished limits (i.e. takes them to colimits).
To see this, let be a $\pjk$-module; then we have

\begin{align*}
\modpjk(\Gamma,\yon_{(\colim_i A_i)}; \cU)
&\cong \modpjk(\Gamma; \cU[\colim_i A_i\,; \,])\\
&\cong \modpjk(\Gamma; \lim_i \cU[A_i\,; \,])\\
&\cong \lim_i \modpjk(\Gamma; \cU[A_i\,;\,])\\
&\cong \lim_i \modpjk(\Gamma, \yon_{A_i}; \cU)\\
&\cong \modpjk(\Gamma,\colim_i (\yon_{A_i}); \cU),
\end{align*}

using the assumption on $\cU$ in the second step.
The claim about $\noy{}$ is dual.

Given $\pjk$, its envelope is the Chu construction

\[ \envpjk=\chu(\modpjk,\cP).\]

$\envpjk$ is a complete and cocomplete $\ast$-autonomous category, contains as a full sub-polycategory, and the inclusion preserves the distinguished tensor and cotensor products and the distinguished limits and colimits.

Just like <ref> except for the final claim, which follows from the formulas for limits and colimits in a Chu construction and <ref><ref>:

\begin{align*}
\lim_i (A^+_i, A^-_i, e_{i}) &= (\lim_i A^+_i, \colim_i A^-_i, \underline{\hspace{1ex}})\\
\colim_i (A^+_i, A^-_i, e_{i}) &= (\colim_i A^+_i, \lim_i A^-_i, \underline{\hspace{1ex}})\qedhere
\end{align*}

We want to combine this with <ref> as before, but there is a complication.
For any limit cone in a closed symmetric monoidal category , we might expect

\begin{align*}
\text{\textquestiondown} \qquad \fsp\cC(\Gamma,\overline\Pi; \Delta, \overline\Sigma, \lim_i A_i)
&= \cC(\Gamma,\Sigma; \Delta,\Pi, \lim_i A_i)\\
&\cong \lim_i \cC(\Gamma,\Sigma; \Delta,\Pi, A_i)\\
&=\lim_i \fsp\cC(\Gamma,\overline\Pi; \Delta, \overline\Sigma, A_i) \qquad ?
\end{align*}

yielding a limit in $\fsp\cC$.
However, the isomorphism in the second line is only valid if $\Delta=\Pi=\emptyset$, whereas to have a limit in $\fsp\cC$ the composite isomorphism must hold for all $\Delta$ and $\Pi$.
Of course, if $\Delta\cup\Pi$ is nonempty, then $\fsp\cC(\Gamma,\overline\Pi; \Delta, \overline\Sigma, \lim_i A_i)$ is empty, as is each $\fsp\cC(\Gamma,\overline\Pi; \Delta, \overline\Sigma, A_i)$ — but the latter only implies that their limit
is empty if the diagram is nonempty!
And indeed, a terminal object in need not be terminal in $\fsp\cC$: the latter requires $\fsp\cC(\Gamma,\overline\Pi;\Delta,\overline\Sigma,1)=1$ always, but the former only ensures that this holds when $\Pi = \Delta = \emptyset$.
Similar considerations apply for colimits,
so the best enhancement of <ref> we can manage is:

Any closed symmetric monoidal category can be fully embedded in a $\ast$-autonomous category by a strong symmetric monoidal closed functor, which preserves any chosen family of nonempty limits and colimits that exist in .

With other choices of $(\cP,\cJ,\cK)$, we can embed other kinds of structures into $\ast$-autonomous categories as well.
For instance:

* Any linearly distributive category can be fully embedded in a $\ast$-autonomous category, preserving tensors, cotensors, and any set of colimits that are preserved in each variable by $\ten$ and limits that are preserved in each variable by $\coten$.

* Any ordinary category can be fully embedded in a $\ast$-autonomous category preserving any set of nonempty limits and colimits.
(Recall from <ref> that this embedding is closely related to the Isbell envelope.)

In the special case when is cartesian closed, of course the terminal object $1$ is also the monoidal unit.
Since the embedding $\cC\into \envcjk$ preserves the monoidal unit, the image of $1\in\cC$ in $\envcjk$ is again the monoidal unit, but it will no longer be terminal.
And if we include binary products in $\cK$, then this embedding preserves both tensor products and binary cartesian products, which coincide in ; hence tensor products and binary cartesian products of objects in the image of  also coincide in $\envcjk$.
However, $\envcjk$ is not itself cartesian monoidal: tensor products and cartesian products of objects not in the image of need not coincide.

§ CONSERVATIVITY

Since closed symmetric monoidal and $\ast$-autonomous categories model intuitionistic and classical linear logic, respectively, <ref> implies a conservativity result.

Classical linear logic with $(-)^\bot, \ten, \coten, \unit, \bot, \hom, \&, \oplus$ is conservative over intuitionistic linear logic with $\ten, \unit, \hom, \&, \oplus$ (but not $\mathbf{0},\top$).

Let and denote the given fragments, and let $T$ be a theory in .
By imposing an appropriate equivalence relation on proofs from $T$ in and respectively, we obtain a closed symmetric monoidal category $\cC_T$ and a $\ast$-autonomous category $\cD_T$, both with binary products and coproducts, and each freely generated by a model of $T$ among categories with the same structure.

By <ref>, $\cC_T$ embeds fully in $\env{\cC_T}$ preserving all the structure.
Since $\env{\cC_T}$ is a nomous model of $T$, this embedding factors up to isomorphism through $\cD_T$.
Now any sequent in the language of over $T$ that is provable in yields a morphism in $\cD_T$ between objects in the image of $\cC_T$.
Hence such a morphism also exists in $\env{\cC_T}$, and thus also in $\cC_T$.

Similarly, we can show that is conservative over any smaller fragment of , and that full MALL is conservative over any of its fragments.
(IMALL is not a fragment of MALL in this sense, since its judgmental structure is different.)

Perhaps surprisingly, <ref> is almost best possible.
It is shown in [28] that classical linear logic with $\mathbf{0}$ (an initial object) and $\hom$ is not conservative over intuitionistic linear logic with the same connectives: the sequent

\[ C \hom ((\mathbf{0}\hom X) \hom A),\, (C\hom B)\hom \mathbf{0} \vdash A \]

is provable in the former but not the latter.
Thus, not every closed symmetric monoidal category with an initial object admits a strong monoidal closed embedding into a $\ast$-autonomous category preserving the initial object.

As a practical matter, conservativity of over says that we can freely use the former to reason about theories in the latter without changing the theorems that are provable.
Semantically, this means that when reasoning about inequalities in a closed symmetric monoidal poset (with binary meets and joins), we may freely assume that it is $\ast$-autonomous without changing the inequalities $p\le q$ that are provable (where $p$ and $q$ are objects of the original poset).
In particular, we can use the syntax of classical linear logic, which can be interpreted in a $\ast$-autonomous poset, to reason about closed symmetric monoidal posets.

Since <ref> is about categories and not just posets, one might hope to similarly use syntaxes for $\ast$-autonomous categories (e.g. term syntaxes for linear logic, or graphical calculi such as proof nets and circuit diagrams) to reason about closed monoidal categories.
And to a limited extent, this is possible.
For instance, since the embedding of a closed symmetric monoidal category in its envelope is faithful, if we have two given morphisms in that can be proven equal using $\ast$-autonomous syntax, then they were already equal in .
Similarly, since this embedding is conservative (in the category-theoretic sense, i.e. isomorphism-reflecting), if we have a morphism in that can be proven invertible using $\ast$-autonomous syntax, then it was already invertible in .

One might hope that since this embedding is also full, we could conclude that given two objects of , if we can construct a morphism between them using $\ast$-autonomous syntax, then that morphism already exists in .
This is true as far as it goes, but there is a problem in that a priori the particular morphism in that we obtain might depend on the particular embedding of into its envelope.
And while the envelope seems in a certain sense canonical, it is by no means the unique embedding of any given in a $\ast$-autonomous category (for instance, if has a zero object, then its embedding in $\chu(\cC,0)$ is a strong symmetric monoidal closed functor).
Thus, with only <ref> there is a certain arbitrariness in the interpretation of $\ast$-autonomous syntax in a closed symmetric monoidal category, which we might hope to avoid.

As noted in the introduction, the most sensible way to ensure this is to show that the universal functor $\Phi:\cC\to\cD$ from to a $\ast$-autonomous category is fully faithful.
In this case, since any fully faithful embedding of in a $\ast$-autonomous category factors through the universal one, the interpretation of $\ast$-autonomous syntax in resulting from any such embedding must coincide with that resulting from $\Phi$.
I do not know a standard name for a theorem of this sort, but since it is a sort of categorification of conservativity, I will call it 2-conservativity (it is also sometimes called “abstract full completeness”).

Note that <ref> implies immediately that $\Phi$ is faithful and conservative, since the faithful and conservative embedding of in its envelope factors through $\Phi$.
We cannot show full-faithfulness of $\Phi$ in the same way, since fully faithful functors are not cancelable.
However, we can use a general technique introduced by Lafont [24] that combines Artin gluing along a restricted Yoneda embedding (a.k.a. a “Kripke logical relation”), as generalized to the $\ast$-autonomous case by [31, 15, 14] using double gluing.

§ DOUBLE GLUING

The name “double gluing” presumably refers to the appearance of two “logical relation” families, but fortuitously it can also be expressed using double categories.
Recall that a double category is a category internal to $\mathsf{Cat}$; by a poly double category we mean a category internal to .
For example, any polycategory induces a poly double category $\dQ\cP$ consisting of the following structure:

* The objects and the horizontal poly-arrows are those of .

* The vertical arrows are the unary and co-unary morphisms of .
(Note that the vertical arrows in any poly double category are only an ordinary category.)

* The 2-cells are “commutative squares” in of the form

\[
\begin{tikzcd}
(A_1,\dots,A_m) \ar[r,"f"]
\ar[d,shift left=7,"u_m"] \ar[d,shift right=7,"u_1"'] \ar[d,phantom,"\cdots"]  &
(B_1,\dots,B_n) \ar[d,shift left=7,"v_n"] \ar[d,shift right=7,"v_1"'] \ar[d,phantom,"\cdots"] \\
(C_1,\dots,C_m) \ar[r,"g"'] &
\end{tikzcd}
\]

i.e. the assertion that $g\circ (u_1,\dots,u_m) = (v_1,\dots,v_n)\circ f$.

Now since the functor is a right adjoint, it preserves internal categories.
Thus any multicategory with a presheaf has a double Chu construction [29]

\[\dChu(\cE,\bbot) \coloneqq \chu(\dQ(\cE,\bbot)). \]

This is a poly double category described as follows.

* Its objects and horizontal poly-arrows are those of $\chu(\cE,\bbot)$.

* A vertical arrow $u:A\to B$ is a pair $(u\p : A\p\to B\p, u\m: A\m\to B\m)$ such that $\uB \circ (u\p,u\m) = \uA$.

A 2-cell

\[
\begin{tikzcd}
(A_1,\dots,A_m) \ar[r,"f"]
\ar[d,shift left=7,"u_m"] \ar[d,shift right=7,"u_1"'] \ar[d,phantom,"\cdots"] \ar[dr,phantom,"\Downarrow\scriptstyle\mu"] &
(B_1,\dots,B_n) \ar[d,shift left=7,"v_n"] \ar[d,shift right=7,"v_1"'] \ar[d,phantom,"\cdots"] \\
(C_1,\dots,C_m) \ar[r,"g"'] &
\end{tikzcd}
\]

consists of a family of commuting squares in :

\[\small\hspace{-2cm}
\begin{tikzcd}
(A_1\p, \dots, A_m\p, B_1\m, \dots, \widehat{B_j\m},\dots B_n\m) \ar[r,"f\p_j"{name=f}]
\ar[d,shift left=28] \ar[d,shift right=28]
\ar[d,phantom,"{\scriptstyle\cdots (u_1\p,\dots,u_m\p,v_1\m,\dots,\widehat{v_j\m},\dots,v_n\m)\cdots}"]
% \ar[dr,phantom,"\Downarrow\scriptstyle\mu"]
B_j\p \ar[d,"v_j\p"] \\
(C_1\p, \dots, C_m\p, D_1\m, \dots, \widehat{D_j\m},\dots D_n\m) \ar[r,"g\p_j"'{name=g}] &
\end{tikzcd}
\qquad
\begin{tikzcd}
(A_1\p , \dots, \widehat{A_i\p},\dots A_m\p , B_1\m, \dots, B_n\m) \ar[r,"f\m_i"{name=f}]
\ar[d,shift left=28] \ar[d,shift right=28]
\ar[d,phantom,"{\scriptstyle\cdots(u_1\p , \dots, \widehat{u_i\p},\dots u_m\p , v_1\m, \dots, v_n\m) \cdots}"]
% \ar[dr,phantom,"\Downarrow\scriptstyle\mu"]
A_i\m \ar[d,"u_i\m"] \\
(C_1\p , \dots, \widehat{C_i\p},\dots C_m\p , D_1\m, \dots, D_n\m) \ar[r,"g\m_i"'{name=g}] &
\end{tikzcd}\hspace{-2cm}
\]

\[\small\hspace{-2cm}
\begin{tikzcd}
(A_1\p, \dots, A_m\p, B_1\m,,\dots B_n\m) \ar[r,"\uf"{name=f}]
\ar[d,shift left=20] \ar[d,shift right=20]
\ar[d,phantom,"{\scriptstyle\cdots (u_1\p,\dots,u_m\p,v_1\m,\dots,v_n\m)\cdots}"]
% \ar[dr,phantom,"\Downarrow\scriptstyle\mu"]
\bbot \ar[d,equals] \\
(C_1\p, \dots, C_m\p, D_1\m,,\dots D_n\m) \ar[r,"\ug"'{name=g}] &
\bbot
\end{tikzcd}
\]

(the last follows from the others unless $m=n=0$, when it is the only condition).

Now let be a polycategory, and $\Lambda:\cD\to \chu(\cE,\bbot)$ a functor, whose action on objects we write as $\Lambda(A) = (L(A),K(A),\lambda_A)$.
On underlying 1-categories, $L$ and $K$ are functors $\cD\to\cE$ and $\cD\to\cE\op$ respectively.

If and are representable multicategories and $\bbot=1$ is the terminal presheaf, then such a $\Lambda$ reduces to the input data of <cit.>.
For applying $\Lambda$ to the universal morphism $(A,B) \to A\ten B$ yields three morphisms in :

\begin{align*}
m&:L(A)\ten L(B) \to L(A\ten B)\\
k&:L(A)\ten K(A\ten B) \to K(B)\\
k'&:L(B)\ten K(A\ten B) \to K(A)
\end{align*}

of which $k$ and $k'$ determine each other by the symmetries.
Applying $\Lambda$ to units and triple tensors makes $m$ a lax symmetric monoidal structure on $L$ and implies that $k$ is a “contraction” as in <cit.>, and these data determine $\Lambda$.

By <ref>, if is a $\ast$-polycategory and $\bbot=1$, a $\ast$-polycategory functor $\Lambda:\cD \to \chu(\cE,1)$ is uniquely determined by a functor $L:\Umulti(\cD)\to \cE$, with $K(A)$ defined as $L(\d A)$.
If and are representable (hence is $\ast$-autonomous), such an $L$ is equivalently a lax symmetric monoidal functor; thus in this case our $\Lambda$ reduces to the input data of <cit.>.
Up to isomorphism,

the same is true when is $\ast$-autonomous without strict duals.

Let $\psi:\bbot_1\to\bbot_2$ be a morphism of presheaves on , and $\Lambda:\cD \to \chu(\cE,\bbot_2)$.
The double gluing $\gl(\Lambda,\psi)$ is the following comma object in the 2-category of poly double categories (whose 2-cells are vertical transformations):

\[
\begin{tikzcd}
\gl(\Lambda,\psi) \ar[r] \ar[d] \ar[dr,phantom,"\Downarrow"] & \chu(\cE,\bbot_1) \ar[d,"\psi"] \\
\cD \ar[r,"\Lambda"'] & \dChu(\cE,\bbot_2).
\end{tikzcd}
\]

Here and $\chu(\cE,\bbot_1)$ are regarded as vertically discrete poly double categories.
Hence so is $\gl(\Lambda,\psi)$, i.e. it is a plain polycategory.
Its objects consist of

* An object $A\o\in \cD$.

* An object $(A\p,A\m, \uA)$ of $\chu(\cE,\bbot_1)$.

* A vertical morphism $(A\p,A\m,\psi\circ\uA) \to (L(A\o),K(A\o),\lambda_A)$ in $\dChu(\cE,\bbot_2)$, consisting of $A\p \to L(A\o)$ and $A\m \to K(A\o)$ in such that the composites $(A\p,A\m) \to \bbot_1 \xto{\psi} \bbot_2$ and $(A\p,A\m) \to (L(A\o),K(A\o)) \xto{\lambda} \bbot_2$ agree.

Similarly, a morphism $(A_1,\dots,A_m) \to (B_1,\dots,B_n)$ in $\gl(\Lambda,\psi)$ consists of

* A morphism $f:(A\o_1,\dots,A\o_m) \to (B\o_1,\dots,B\o_n)$ in .

* A morphism $(f\p_j,f\m_i,\uf)$ in $\chu(\cE,\bbot_1)$.

* The following squares commute:

\begin{equation}\label{eq:glsq1}
\begin{tikzcd}
(\hspace{3mm}A_1\p\hspace{3mm}, \dots, \hspace{2mm}A_m\p\hspace{2mm}, \hspace{2mm}B_1\m\hspace{2mm}, \dots, \hspace{2mm}\widehat{B_j\m}\hspace{2mm},\dots \hspace{3mm}B_n\m\hspace{3mm}) \ar[r,"f\p_j"{name=f}]
\ar[d,shift left=38] \ar[d,shift right=38]
\ar[d,shift left=18,phantom,"\cdots"]
\ar[d,shift right=27,phantom,"\cdots"]
\ar[d,shift right=17]
\ar[d,shift right=3]
% \ar[d,phantom,"{\scriptstyle\cdots (u_1\p,\dots,u_m\p,v_1\m,\dots,\widehat{v_j\m},\dots,v_n\m)\cdots}"]
% \ar[dr,phantom,"\Downarrow\scriptstyle\mu"]
B_j\p \ar[d] \\
(L(A\o_1), \dots, L(A\o_m), K(B\o_1), \dots, \widehat{K(B\o_j)},\dots K(B\o_n)) \ar[r,"\Lambda(f)\p_j"'{name=g}] &
\end{tikzcd}
\end{equation}

\begin{equation}\label{eq:glsq2}
\begin{tikzcd}
(\hspace{3mm}A_1\p\hspace{3mm} , \dots, \hspace{2mm}\widehat{A_i\p}\hspace{2mm},\dots \hspace{2mm}A_m\p\hspace{2mm} ,\hspace{2mm} B_1\m\hspace{2mm}, \dots, \hspace{3mm}B_n\m\hspace{3mm}) \ar[r,"f\m_i"{name=f}]
\ar[d,shift left=38] \ar[d,shift right=38]
\ar[d,shift right=18,phantom,"\cdots"]
\ar[d,shift left=26,phantom,"\cdots"]
\ar[d,shift left=15]
\ar[d,shift left=2]
% \ar[d,phantom,"{\scriptstyle\cdots(u_1\p , \dots, \widehat{u_i\p},\dots u_m\p , v_1\m, \dots, v_n\m) \cdots}"]
% \ar[dr,phantom,"\Downarrow\scriptstyle\mu"]
A_i\m \ar[d] \\
(L(A\o_1) , \dots, \widehat{L(A\o_i)},\dots L(A\o_m) , K(B\o_1), \dots, K(B\o_n)) \ar[r,"\Lambda(f)\m_i"'{name=g}] &
\end{tikzcd}
\end{equation}

\begin{equation}\label{eq:glsq3}
\begin{tikzcd}
(\hspace{3mm}A_1\p\hspace{3mm}, \dots, \hspace{2mm}A_m\p\hspace{2mm}, \hspace{2mm}B_1\m\hspace{2mm}, \dots, \hspace{3mm}B_n\m\hspace{3mm}) \ar[r,"\uf"{name=f}]
\ar[d,shift left=28] \ar[d,shift right=28]
\ar[d,shift left=15,phantom,"\cdots"]
\ar[d,shift right=17,phantom,"\cdots"]
\ar[d,shift right=8]
\ar[d,shift left=5]
% \ar[d,phantom,"{\scriptstyle\cdots (u_1\p,\dots,u_m\p,v_1\m,\dots,\widehat{v_j\m},\dots,v_n\m)\cdots}"]
% \ar[dr,phantom,"\Downarrow\scriptstyle\mu"]
\bbot_1 \ar[d,"\psi"] \\
(L(A\o_1), \dots, L(A\o_m), K(B\o_1), \dots, K(B\o_n)) \ar[r,"\underline{\Lambda(\smash{f})}"'{name=g}] &
\bbot_2
\end{tikzcd}
\end{equation}

(the last follows from the others unless $m=n=0$, when it is the only condition).

Suppose is representable and closed with pullbacks, and $\bbot_1$ and $\bbot_2$ are either both terminal ($\bbot_1=\bbot_2=1$) or both representable $(\bbot_1 = \yon_{\bot_1}$ and $\bbot_2 = \yon_{\bot_2})$.
Then tensor products, cotensor products, duals, and internal-homs exist in $\gl(\Lambda,\psi)$ insofar as they do for the relevant underlying objects in .
In particular, if is $\ast$-autonomous, so is $\gl(\Lambda,\psi)$.

When $\bbot_1$ and $\bbot_2$ are terminal, we use the formulas from <cit.>.
When they are representable, we modify the formulas slightly; for tensor products we have

\[ (A\ten B)\p = A\p \ten B\p \to L(A\o) \ten L(B\o) \to L(A\o\ten B\o) \]

and the limit of the following diagram (drawn in the middle):

\[\small
\begin{tikzcd}[column sep={2.6cm,between origins}]
&& (A\p \mathord{\ten} B\p) \mathord{\hom} \bot_1 & &\\
& A\p \mathord{\hom} B\m \ar[dl] \ar[ur] & (A\mathord{\ten} B)\m \ar[l,dashed] \ar[r,dashed] \ar[d,dashed] & B\p \mathord{\hom} A\m \ar[dr] \ar[ul]\\
A\p \mathord{\hom} K(B\o) & L(A\o) \mathord{\hom} K(B\o) \ar[l] & K(A\o\mathord{\ten} B\o) \ar[l] \ar[r] & L(B\o) \mathord{\hom} K(A\o) \ar[r] & B\p \mathord{\hom} K(A\o).
\end{tikzcd}
\]

The unit consists of $\unit\p = \unit \to L(\unit)$ and the pullback

\[
\begin{tikzcd}
\unit\m \ar[rrr] \ar[d] \drpullback & & & \bot_1 \ar[d] \\
K(\unit) \ar[r,"\cong"'] & \unit\ten K(\unit) \ar[r] & L(\unit) \ten K(\unit) \ar[r,"\lambda"'] & \bot_2\mathrlap.
\end{tikzcd}
\]

The dual of $(A\o,A\p,A\m,\uA)$ is $(\d {(A\o)}, A\m, A\p, \uA\sigma)$, and for the internal-hom we have

\[\small
\begin{tikzcd}[column sep={2.6cm,between origins}]
&& (A\p \mathord{\ten} B\m) \mathord{\hom} \bot_1 & &\\
& A\p \mathord{\hom} B\p \ar[dl] \ar[ur] & (A\mathord{\hom} B)\p \ar[l,dashed] \ar[r,dashed] \ar[d,dashed] & B\m \mathord{\hom} A\m \ar[dr] \ar[ul]\\
A\p \mathord{\hom} L(B\o) & L(A\o) \mathord{\hom} L(B\o) \ar[l] & L(A\o\mathord{\hom} B\o) \ar[l] \ar[r] & K(B\o) \mathord{\hom} K(A\o) \ar[r] & B\m \mathord{\hom} K(A\o).
\end{tikzcd}
\]

\[ (A\hom B)\m = A\p \ten B\m \to L(A\o) \ten K(B\o) \to K(A\o\hom B\o). \]

We leave cotensor products to the reader.

Double gluing is usually described only when $\bbot_1=\bbot_2=1$, but our more general version appears implicitly in at least one place.
Specifically, consider <ref> with $L = \cC(\unit,-)$ and $K = \cC(-,J)$ for some $J$, as in <cit.>.
Then every object $\Lambda(A) = (LA,KA)$ comes with a pairing $LA\times KA = \cC(\unit,A) \times \cC(A,J) \to \cC(\unit,J)$, which is respected by every morphism in the image of $\Lambda$; thus the codomain of $\Lambda$ lifts to $\chu(\fSet,\bot_2)$ where $\bot_2=\cC(\unit,J)$.
Now for any $F\subseteq \cC(\unit,J)$ we can take $\psi : \bot_1 = F \into \cC(\unit,J) = \bot_2$, and the resulting $\gl(\Lambda,\psi)$ coincides (modulo a restriction to monomorphisms) with the slack orthogonality category of the focused orthogonality on $\gl(\Lambda,1)$ determined by $F$ as in <cit.>.

§ 2-CONSERVATIVITY

Let be a polycategory with as in <ref>, and let $\Phi:\cP\to\cD$ be its universal functor to a nomous category.
That is, $\Phi$ is a polycategory functor preserving the tensor and cotensor products in (up to isomorphism), and such that any polycategory functor $\cP \to \cQ$ that preserves and where is $\ast$-autonomous factors essentially uniquely through $\Phi$.
This “up to isomorphism” version is categorically “correct”, and seems to be necessary since the functor $\Xi$ below does not preserve strictly.
The existence of such $\Phi$ follows from 2-categorical algebra [3].

The universal functor $\Phi:\cP\to\cD$ from any $(\cP,\cJ)$ to a nomous category is fully faithful.

Following Lafont's technique, we will construct the (double) gluing of $\cD$ along the restricted (polycategorical) Yoneda embedding of $\Phi$, and then lift $\Phi$ to a functor $\Xi$ landing in this gluing category that preserves .
By the universal property of $\cD$, it will follow that this gluing category has a section, a “logical relations” functor that assigns in particular to each morphism in a unique morphism in that maps onto it, showing full-faithfulness of $\Phi$.

For any -module , we write $\cU[\Phi]$ for the -module with $\cU[\Phi](\Gamma;\Delta) = \cU(\Phi(\Gamma);\Phi(\Delta))$.
This defines a functor $(-)[\Phi]:\mod\cD \to \modp$; and if respects the tensor and cotensor products of , then $\cU[\Phi]$ is a $(\cP,\cJ)$-module since $\Phi$ preserves .
Now we let $\Lambda$ be the composite polycategory functor

\[ \cD \xto{(\yon,\scriptnoy{},\gm)} \env\cD = \chu(\mod\cD,\cD) \xto{(-)[\Phi]} \chu(\modp,\cD[\Phi]), \]

where $(\mod\cD,\cD) \to (\modp,\cD[\Phi])$ is induced by $\Phi$.
Thus on objects we have

\begin{equation}
\Lambda(R) = (L(R),K(R),\lambda_R) = (\cD[\,;R][\Phi], \cD[R;\,][\Phi], \gamma_{\Phi R}).\label{eq:fcLK}
\end{equation}

Note that $\Lambda$ lands in $\chu(\modpj,\cD[\Phi])$.
Now $\Phi$ also induces a map $\phi : \cP \to \cD[\Phi]$ in .
Since is $\ast$-autonomous and $\modpj$ is representable and closed with pullbacks, the double gluing category $\gl(\Lambda,\phi)$ is $\ast$-autonomous.

We now define a functor $\Xi : \cP \to \gl(\Lambda,\phi)$.
By the definition of $\gl(\Lambda,\phi)$ and the universal property of comma objects, to define $\Xi$ it suffices to give the following diagram in poly double categories (most of which are vertically discrete):

\[
\begin{tikzcd}
\cP \ar[r,"{(\yon,\scriptnoy{},\gm)}"] \ar[d,"\Phi"'] \ar[drr,phantom,near end,"\Downarrow"] & \envpj \ar[r,equals] & \chu(\modpj,\cP) \ar[d,"\phi"] \\
\cD \ar[rr,"\Lambda"'] && \dChu(\modpj,\cD[\Phi])
\end{tikzcd}
\]

The necessary 2-cell has components
\( \yon_A \to \yon_{\Phi A}[\Phi] \) and \( \noy{A} \to \noy{\Phi A}[\Phi] \), which
we take to be the action of $\Phi$ on hom-sets.
Thus $\Xi(A)$ consists of $\Phi A\in \cD$, $(\yon_A, \noy A, \gamma_A) \in \chu(\modpj,\cP)$, and the maps

\begin{align}
\yon_A &= \cP[\,; A] \to \cD[\Phi][\,;A] = \cD[\,;\Phi A][\Phi] = \yon_{\Phi A}[\Phi] \label{eq:theta1}\\
\noy A &= \cP[A;\,] \to \cD[\Phi][A;\,] = \cD[\Phi A;\,][\Phi] = \noy{\Phi A}[\Phi] \label{eq:theta2}
\end{align}

We claim that $\Xi$ preserves the tensor and cotensor products in .
For the tensors, we use that $\Phi$ and $\yon$ preserve them, and also need to calculate the limit

\[\small
\begin{tikzcd}[column sep={2.6cm,between origins}]
&& (\yon_A \mathord{\ten} \yon_B) \mathord{\hom} \cP & &\\
& \yon_A \mathord{\hom} \noy{B} \ar[dl] \ar[ur] & \bullet \ar[l,dashed] \ar[r,dashed] \ar[d,dashed] & \yon_B \mathord{\hom} \noy{A} \ar[dr] \ar[ul]\\
\yon_A \mathord{\hom} K(\Phi B) &
% L(\Phi A) \mathord{\hom} K(\Phi B) \ar[l]
& K(\Phi A\mathord{\ten} \Phi B) \ar[ll] \ar[rr] &
% L(\Phi B) \mathord{\hom} K(\Phi A) \ar[r]
& \yon_B \mathord{\hom} K(\Phi A).
\end{tikzcd}
\]

Using (<ref>) and (<ref>), this becomes

\[\small
\begin{tikzcd}[column sep={2.6cm,between origins}]
&& \cP[A,B;] & &\\
& \cP[A,B;] \ar[dl] \ar[ur] & \bullet \ar[l,dashed] \ar[r,dashed] \ar[d,dashed] & \cP[A,B;] \ar[dr] \ar[ul]\\
\cD[\Phi B;][\Phi][A;] \ar[d,"\cong"] &
% \cD[;\Phi A][\Phi] \mathord{\hom} \cD[\Phi B;][\Phi] \ar[l]
& \cD[\Phi A\mathord{\ten} \Phi B;][\Phi] \ar[ll] \ar[rr] \ar[d,"\cong"] &
% \cD[;\Phi B][\Phi] \mathord{\hom} \cD[\Phi A;][\Phi] \ar[r]
& \cD[\Phi A;][\Phi][B;] \ar[d,"\cong"] \\
\cD[\Phi][A,B;] && \cD[\Phi][A,B;] \ar[ll] \ar[rr] && \cD[\Phi][A,B;]
\end{tikzcd}
\]

whose limit is $\cP[A,B;]\cong \noy{A\ten B}$.
For a unit, we instead consider the pullback

\[
\begin{tikzcd}
\bullet \ar[r] \ar[d] \drpullback & \cP \ar[d] \\
\cD[\Phi\unit;][\Phi] \ar[r] % \ar[r,"\cong"'] &
% \unit\ten \cD[\Phi\unit;][\Phi]  \ar[r] &
%\cD[;\Phi\unit][\Phi] \ten \cD[\Phi\unit;][\Phi] \ar[r,"\lambda"']
& \cD[\Phi].
\end{tikzcd}
\]

But the bottom map is an isomorphism, hence the pullback is isomorphic to $\cP$, which is isomorphic to $\cP[\unit;] = \noy{\unit}$.
Cotensors are dual.

Now, since the composite $\cP \xto{\Xi} \gl(\Lambda,\cP) \to \cD$ is equal to $\Phi$, we can extend $\Xi$ by the universal property of $\cD$ to a functor $\Xi':\cD \to \gl(\Lambda,\cP)$.

\begin{equation*}
\begin{tikzcd}
&& \gl(\Lambda,\cP) \ar[d] \\
\cP \ar[r,"\Phi"'] \ar[urr,"\Xi",bend left=5] &
\cD \ar[ur,dashed,"\Xi'"'] \ar[r,equals] & \cD.
\end{tikzcd}%\label{eq:ext-sect}
\end{equation*}

By the universal property of $\gl(\Lambda,\cP)$, this means we have a diagram

\[
\begin{tikzcd}
\cP \ar[d,"\Phi"'] \ar[r,"{(\yon,\scriptnoy{},\gm)}"] \ar[drr,phantom,near end,"\Downarrow\scriptstyle\mu"] & \envpj \ar[r,equals] &
\chu(\modpj,\cP) \ar[d,"\phi"] \\
\cD \ar[urr,bend left=5,dashed,"\Xi'",near start] \ar[rr,"\Lambda"'] && \dChu(\modpj,\cD[\Phi])
\end{tikzcd}
\]

where $\mu\Phi$ equals (<ref>)–(<ref>).
This determines the components of $\mu$ on objects $\Phi A$; its naturality on all morphisms in between such objects then entails multiple commuting squares like (<ref>)–(<ref>).
Considering only those like (<ref>), we conclude that the quadrilateral involving $\Xi'$ in the following diagram commutes:

\[\small\hspace{-2cm}
\begin{tikzcd}[column sep={3.5cm,between origins}]
\cP(A_1,\dots,A_m;B_1,\dots,B_n) \ar[d,"\Phi"'] \ar[rr,"\cong"] &&
% \envpj(\gm_\Gamma;\gm_\Delta) \ar[r] &
\modpj(\yon_{A_1},\dots,\yon_{A_m},\noy{B_1},\dots,\noy{B_n},\dots;\cP) \ar[d] \\
\cD(\Phi A_1,\dots,\Phi A_m;\Phi B_1,\dots,\Phi B_n) \ar[dr] \ar[urr,dashed,"\Xi'"] \ar[rr,dotted,"\cong"'] &&
\modpj(\yon_{A_1},\dots,\yon_{A_m},\noy{B_1},\dots,\noy{B_n};\cD[\Phi]) \\
% \dChu(\modpj,\cD[\Phi])(\Lambda\Phi(\Gamma);\Lambda\Phi(\Delta)) \ar[r] &
\modpj(\cD[\Phi][;A_1],\dots,\cD[\Phi][;A_m],\cD[\Phi][B_1;],\dots,\cD[\Phi][B_n;];\cD[\Phi]) \ar[ur]
\end{tikzcd}\hspace{-2cm}
\]

Now the two horizontal arrows are isomorphisms by the Yoneda lemma, <ref>.
Thus, by the 2-out-of-6 property for isomorphisms, the left-hand vertical map

\[ \cP(A_1,\dots,A_m;B_1,\dots,B_n) \xto{\Phi} \cD(\Phi A_1,\dots,\Phi A_m;\Phi B_1,\dots,\Phi B_n) \]

is also an isomorphism; i.e. $\Phi$ is fully faithful.

Most of the proof would work using the traditional $\gl(\Lambda,1)$ instead of our $\gl(\Lambda,\phi)$.
The first difference is that when showing that $\Xi$ preserves , omitting $(\yon_A \ten \yon_B) \hom \cP$ from the diagram changes the limit to the kernel-pair of $\cP[A,B;] \to \cD[\Phi][A,B;]$.
But as noted in <ref>, we already know $\Phi$ is faithful; so this morphism is monic, hence its kernel pair is just its domain.

The second difference is that the squares like (<ref>) would carry no information.
We could use the squares like (<ref>)–(<ref>) instead — unless $m=n=0$, in which case there are no such squares!
We can ignore this case if includes a unit or counit, as it usually does; but it seems preferable to have a proof that works in general.

Let be a closed symmetric monoidal category and $\Phi:\cC\to\cD$ its universal functor to a $\ast$-autonomous one.
Then $\Phi$ is fully faithful.

A closed symmetric monoidal functor from to a $\ast$-autonomous category factors essentially uniquely through $(\fsp\cC,\cJ)$.
Thus $\Phi':\fsp\cC\to\cD$ is the universal functor from $(\fsp\cC,\cJ)$ to a $\ast$-autonomous category; now apply <ref>.

To emphasize how this proof deals with the internal-homs, we check explicitly that the induced $\Xi:\cC\to \gl(\Lambda,\phi)$ preserves them.
We must inspect the limit

\[\small
\begin{tikzcd}[column sep={2.6cm,between origins}]
&& (\yon_A \mathord{\ten} \noy{B}) \mathord{\hom} \fsp\cC & &\\
& \yon_A \mathord{\hom} \yon_B \ar[dl] \ar[ur] & \bullet \ar[l,dashed] \ar[r,dashed] \ar[d,dashed] & \noy{B} \mathord{\hom} \noy{A} \ar[dr] \ar[ul]\\
\yon_A \mathord{\hom} \cD[;B][\Phi] &
% \cD[;A][\Phi] \mathord{\hom} \cD[;B][\Phi] \ar[l]
& \cD[;A\mathord{\hom} B][\Phi] \ar[ll] \ar[rr] &
% \cD[B;][\Phi] \mathord{\hom} \cD[A;][\Phi] \ar[r]
& \noy{B} \mathord{\hom} \cD[A;][\Phi].
\end{tikzcd}
\]

which by (<ref>) and (<ref>) becomes

\[\small
\begin{tikzcd}[column sep={2.6cm,between origins}]
&& \fsp\cC[A;B] & &\\
& \fsp\cC[A;B] \ar[dl] \ar[ur] & \bullet \ar[l,dashed] \ar[r,dashed] \ar[d,dashed] & \fsp\cC[A;B] \ar[dr] \ar[ul]\\
\cD[;\Phi B][\Phi][A;] \ar[d,"\cong"] &
% \cD[;A][\Phi] \mathord{\hom} \cD[;B][\Phi] \ar[l]
& \cD[;\Phi(A\mathord{\hom} B)][\Phi] \ar[ll] \ar[rr]\ar[d,"\cong"] &
% \cD[B;][\Phi] \mathord{\hom} \cD[A;][\Phi] \ar[r]
& \cD[\Phi A;][\Phi][;B]\ar[d,"\cong"]\\
\cD[\Phi][A;B] && \cD[\Phi][A;B] \ar[ll] \ar[rr] && \cD[\Phi][A;B],
\end{tikzcd}
\]

whose limit is $\fsp\cC[A;B] \cong \fsp\cC[;A\mathord{\hom} B] = \yon_{A\hom B}$.
We also need to check that

\[ \yon_A \ten \noy{B} \to \cD[;\Phi A \hom \Phi B][\Phi]
\quad\text{is isomorphic to}\quad
\noy{A\hom B} \to \cD[;\Phi(A\hom B)][\Phi]. \]

But by <ref>, we have
\( \noy{A\hom B} = \noy{\Abar \coten B} \cong \noy{\Abar} \ten \noy{B} \cong \yon_A \ten \noy{B}. \)

This is the crucial point: the polycategorical framework supplies a contravariant Yoneda embedding $\noy{}$ that maps internal-homs to tensor products.

It is claimed in [15, 14] that 2-conservativity for $\ast$-autonomous extensions of closed symmetric monoidal categories can be proven using double gluing into an ordinary presheaf category.
However, it seems that this does not work.
An ordinary Yoneda embedding has no contravariant version like $\noy{}$, so the “dual parts” of the functor $\Xi$ have to be chosen “tautologically”; but then $\Xi$ fails to preserve the internal-homs.
In the notation of <cit.>, $(\dP_A \hom \dP_B)_t(X)$ is the set of morphisms $\dI X\to \dI A \ten (\dI B)^\bot$ in $\dC_1$ that factor as $(\dI f\ten g) \circ \dI h$ for some $h\in \dC_0(X,Y\ten Z)$, $f\in \dC_0(Y,A)$, and $g\in \dC_1(\dI Z, (\dI B)^\bot)$, whereas $(\dP_{A\hom B})_t(X)$ is the set of all morphisms in $\dC_1(\dI X, \dI A \ten (\dI B)^\bot)$.
There seems no reason why every such morphism should factor in that way.

<ref> also specializes to other polycategorical structures.
For instance, we have the following result (shown in [2] by cut-elimination).

The universal functor $\Phi:\cP\to\cD$ from a linearly distributive category to a $\ast$-autonomous one is fully faithful.

By [9], $\cP$ can be regarded as a representable polycategory.
Now apply <ref> with all tensors and cotensors in .

We can also include a family of limits and colimits by double gluing with $\modpjk$ instead.
The formulas in <cit.> for products and coproducts in double gluing categories still work, as do similar ones for other limits and colimits, and the functor $\Xi$ preserves them.
Of course, as in <ref>, only nonempty limits and colimits in a multicategory induce polycategorical ones in $\fsp\cC$.

[1]
Michael Barr.
$\ast$-autonomous categories, volume 752 of Lecture Notes
in Mathematics.
Springer, 1979.

[2]
R. Blute, R. Cockett, R. Seely, and T. Trimble.
Natural deduction and coherence for weakly distributive categories.
J. Pure and Appl. Algebra, 113:229–296, 1996.

[3]
R. Blackwell, G. M. Kelly, and A. J. Power.
Two-dimensional monad theory.
J. Pure Appl. Algebra, 59(1):1–41, 1989.

[4]
Richard Blute.
Proof nets and coherence theorems.
In Category Theory and Computer Science, pages 121–137,
Berlin, Heidelberg, 1991. Springer Berlin Heidelberg.

[5]
Richard Blute.
Linear logic, coherence and dinaturality.
Theoretical Computer Science, 115(1):3–41, 1993.

[6]
John Baez and Mike Stay.
Physics, topology, logic and computation: A Rosetta stone.
In New Structures for Physics, volume 813 of Lecture Notes
in Physics, pages 95–174. Springer, 2011.

[7]
Po-Hsaing Chu.
Constructing $\ast$-autonomous categories.
In $\ast$-autonomous categories, volume 752 of Lecture
Notes in Mathematics, chapter Appendix. Springer-Verlag, 1979.

[8]
J.R.B. Cockett, J. Koslowski, and R.A.G. Seely.
Morphisms and modules for poly-bicategories.
Theory Appl. Categ., 11(2):15–74, 2003.

[9]
Robin Cockett and Robert Seely.
Weakly distributive categories.
Journal of Pure and Applied Algebra, 114(2):133–173, 1997.

[10]
Brian Day.
On closed categories of functors.
In Reports of the Midwest Category Seminar, IV, Lecture Notes
in Mathematics, Vol. 137, pages 1–38. Springer, Berlin, 1970.

[11]
Brian Day.
A reflection theorem for closed categories.
J. Pure Appl. Algebra, 2(1):1–11, 1972.

[12]
Gabriel C. Drummond-Cole and Philip Hackney.
Dwyer–Kan homotopy theory for cyclic operads.
arXiv:1809.06322, 2018.

[13]
P. J. Freyd and G. M. Kelly.
Categories of continuous functors. I.
J. Pure Appl. Algebra, 2:169–191, 1972.

[14]
M. Hasegawa.
Categorical glueing and logical predicates for models of linear
Preprint RIMS-1223, Kyoto University, 1999.
<http://www.kurims.kyoto-u.ac.jp/ hassei/papers/full.pdf>.

[15]
Martin Hyland and Andrea Schalk.
Glueing and orthogonality for models of linear logic.
Theoretical Computer Science, 294(1):183 – 231, 2003.
Category Theory and Computer Science.

[16]
Dominic J.D. Hughes.
Simple free star-autonomous categories and full coherence.
Journal of Pure and Applied Algebra, 216(11):2386 – 2410,

[17]
J.M.E. Hyland.
Proof theory in the abstract.
Annals of Pure and Applied Logic, 114:43–78, 2002.

[18]
John R. Isbell.
Structure of categories.
Bull. Amer. Math. Soc., 72:619–655, 1966.

[19]
M. Hasegawa J.R.B. Cockett and R.A.G. Seely.
Coherence of the double involution on $\ast$-autonomous categories.
Theory and Applications of Categories, 17(2):17–29, 2006.

[20]
André Joyal, Ross Street, and Dominic Verity.
Traced monoidal categories.
Math. Proc. Cambridge Philos. Soc., 119(3):447–468, 1996.

[21]
G. M. Kelly.
Basic concepts of enriched category theory, volume 64 of London Mathematical Society Lecture Note Series.
Cambridge University Press, 1982.
Also available online in Reprints in Theory and Applications of
Categories, No. 10 (2005) pp. 1-136.

[22]
G. M. Kelly and Stephen Lack.
On property-like structures.
Theory Appl. Categ., 3(9):213–250, 1997.

[23]
G.M. Kelly and S. Maclane.
Coherence in closed categories.
Journal of Pure and Applied Algebra, 1(1):97 – 140, 1971.

[24]
Yves Lafont.
Logiques, catégories & machines : implantation de langages
de programmation guidée par la logique catégorique.
PhD thesis, Paris 7, 1988.

[25]
Duško Pavlović.
Chu I: cofree equivalences, dualities, and $\ast$-autonomous
Math. Struct. in Comp. Science, 11, 1993.

[26]
Uday S. Reddy.
Acceptors as values.
<http://www.cs.bham.ac.uk/ udr/>, 1991.

[27]
Uday S. Reddy.
A typed foundation for directional logic programming.
In E. Lamma and P. Mello, editors, Extensions of Logic
Programming, pages 282–318, Berlin, Heidelberg, 1993. Springer Berlin

[28]
Harold Schellinx.
Some syntactical observations on linear logic.
Journal of Logic and Computation, 1(4):537–559, 1991.

[29]
Michael Shulman.
The 2-Chu-Dialectica construction and the polycategory of
multivariable adjunctions.
Theory Appl. Categ., 35(4):89–136, 2020.

[30]
M.E. Szabo.
Communications in Algebra, 3(8):663–689, 1975.

[31]
Audrey Tan.
Full completeness for models of Linear Logic.
PhD thesis, Cambridge University, 1998.

[32]
Todd Trimble.
Linear Logic, Bimodules, and Full Coherence for Autonomous
PhD thesis, Rutgers University, 1994.