To obtain the internal logic of a topos (roughly speaking), we associate a type of free variable with an object, and a statement about such a variable with a subobject of that object. Intuitively, the subobject represents the possible values of the variable for which the statement is true. By associating logical operators with operations on subobjects, we obtain an internal logic with which to reason about the relationships between subobjects of all objects in the topos.
The internal logic of monoidal categories (optionally symmetric, closed, *-autonomous, etc), as usually described, is different. Here, a proposition of linear logic is associated with an object in the monoidal category, rather than a subobject. The monoidal category is therefore analogous to the poset of subobjects of a single object in a topos, rather than to the whole original topos. It is possible to extend this framework (eg Seely p. 10) using a base category $\bf S$ corresponding to free variable types, and an indexed category containing a monoidal category for each element of $\bf S$. However, this base category is not itself monoidal.
Is there a type of internal logic that lets us reason about the relationships of subobjects of any object in a monoidal base category?
An example application would be in quantum mechanics. A statement about a quantum system with Hilbert space ${\bf H}_A$ corresponds to a subspace $S_A \subseteq {\bf H}_A$. If we a have second system with Hilbert space ${\bf H}_B$ side by side with our first system, then a statement about both of them corresponds to a subspace of ${\bf H}_A \otimes {\bf H}_B$. Given subspaces $S_A \subseteq {\bf H}_A$ and $S_B \subseteq {\bf H}_B$, we can define a subspace $S_A \otimes S_B \subseteq {\bf H}_A \otimes {\bf H}_B$ as the span of $\{ a\otimes b | a \in S_A, b \in S_B\}$. Alternatively, if a single quantum system could be either in a state of type A or type B, then its Hilbert space is ${\bf H}_A \oplus{\bf H}_B$. Again, given two subspaces $S_A \subseteq {\bf H}_A$ and $S_B \subseteq {\bf H}_B$, we can define a subspace $S_A \oplus S_B \subseteq {\bf H}_A \oplus {\bf H}_B$.
I guess a way to ask the question is this. Given a monoidal category $M$ (optionally symmetric, closed, *-autonomous, etc), is there a monoidal functor that maps $M$ to a monoidal category representing the subobjects of all objects of $M$? Thus, given two objects $A$ and $B$ of $M$, and subobjects $S_A \in Sub(A)$, $S_B \in Sub(B)$, we could obtain $S_A \otimes S_B \in Sub(A \otimes B)$, $S_A \oplus S_B \in Sub(A \oplus B)$, $S_A^\bot \in Sub(A^*)$, $S_A \rightarrow S_B \in Sub(A \rightarrow B)$, etc. We could then use the linear logic of the second category to reason about subobjects of all objects in $M$.
