This is the first post in a series of posts on doing enriched indexed category theory and using the notion of an internal language to make this look relatively mundane. The internal language aspects are useful for other purposes too, as will be illustrated in this post, for example. This is related to the post Category Theory, Syntactically. In particular, it can be considered half-way between the unary theories and the finite product theories described there.
First in this series – this post – covers the internal language of a monoidal category. This is fairly straightforward, but it already provides some use. For example, the category of endofunctors on a category is a strict monoidal category, and so we can take a different perspective on natural transformations. This will also motivate the notions of a (virtual) bicategory and an actegory. Throughout this post, I’ll give a fairly worked example of turning some categorical content into rules of a type-/proof-theory.
The second post will add indexing to the notion of monoidal category and introduce the very powerful and useful notion of an indexed monoidal category.
The third post will formulate the notion of categories enriched in an indexed monoidal category and give the definitions which don’t require any additional assumptions.
The fourth post will introduce the notion and internal language for an indexed cosmos. Normally, when we do enriched category theory, we want the category into which we’re enriching to not be just a monoidal category but a cosmos. This provides many additional properties. An indexed cosmos is just the analogue of that for indexed monoidal categories.
The fifth post will then formulate categorical concepts for our enriched indexed categories that require some or all of these additional properties provided by an indexed cosmos.
At some point, there will be a post on virtual double categories as they (or, even better, augmented virtual double categories) are what will really be behind the notion of enriched indexed categories we’ll define. Basically, we’ll secretly be spelling out a specific instance of the |\mathsf{Mod}| construction.
Fix a monoidal category called |\V|.
The internal language of a monoidal category is quite simple to describe1. We’ll write terms in context. The term $$\begin{align} a_1 : A_1, \dots, a_n : A_n \vdash E : B\end{align}$$ will represent an arrow |A_1 \otimes \cdots \otimes A_n \to B| in |\V|. The |n = 0| case will be represented by omitting the context and will correspond to an arrow from the unit, |I|. However, there’s a catch. The term |E| must use all the variables |a_1, \dots, a_n| exactly once and in the order that they are listed in the context. (The |\mathsf{match}| construct will make this more complicated. Ultimately, a one-dimensional syntax isn’t that well suited to this situation.) For example, $$\begin{align}a_1 : A_1, a_2: A_2 \vdash \mathsf f(a_2, a_1) : B, \quad a : A_1 \vdash \mathsf g(a, a) : B, \quad \text{and} \quad a : A \vdash \mathsf b : B\end{align}$$ are all invalid. We’ll call the context the linear context, consisting of linear variables with linear types, which we’ll usually represent with the metavariable |\Delta|. The naming comes from the connections to ordered linear logic.
Substituting for the linear variables, written |E[E_1/a_1,\dots,E_n/a_n]|, corresponds to the composition |E \circ (E_1 \otimes \cdots \otimes E_n)|. You can work out what associativity and unit laws of composition would look like. It should be noted, though, that this is a meta-theorem. Substitution is defined in the typical, syntactic way, and we’d need to prove that for every term the interpretation of the result of substituting into that term is equal to the composition of the interpretations.
If we replaced arrows |A_1 \otimes \cdots \otimes A_n \to B| in a monoidal category with multiarrows |(A_1, \dots, A_n) \to B| in a multicategory2, then we’d be done. However, monoidal categories correspond to representable multicategories. If we write, |\mathcal C(A_1, \dots, A_n; B)| for the set of multiarrows |(A_1, \dots, A_n) \to B| in the multicatgory |\mathcal C|, then |\mathcal C| being representable means we have $$\begin{align} \mathcal C(A_1, \dots, A_m, B_1, \dots, B_n, C_1, \dots, C_p; D) \cong \mathcal C(A_1, \dots, A_m, B_1 \otimes \cdots \otimes B_n, C_1, \dots, C_p; D) \end{align}$$ natural in |D| and multinatural in the |A_i| and |C_i|. This implies that every |n|-ary arrow is equivalent to a unary arrow.
Since it’s useful to know, I’ll go into some detail on how we derive natural-deduction-style rules from this categorical data. First, we note that the above natural isomorphism (at least when |m=0| and |p=0|) has the form of a universal property using representability and, specifically, is a mapping-out property. That is, we are saying that the functor |\mathcal C(B_1, \dots, B_n; \_)| is represented by |B_1 \otimes \cdots \otimes B_n|. Let’s call the left to right direction of the above natural isomorphism |\varphi|. While this universal property can, of course, be represented by the natural isomorphism as above, it can also be equivalently represented by a universal element. Namely, one particularly notable choice for |D| is |B_1 \otimes \cdots \otimes B_n| itself, at which point we can consider |\eta = \varphi^{-1}(id_{B_1 \otimes \cdots \otimes B_n}) : (B_1, \dots, B_n) \to B_1 \otimes \cdots \otimes B_n|. By using naturality of |\varphi^{-1}|, we can easily show that |\varphi^{-1}(f) = f \circ \eta|. To witness the fact that |\varphi^{-1}(\varphi(f)) = f|, we need |\varphi(f) \circ \eta = f|. We’ve now shown that a natural transformation |\varphi| as above and an element (in this case a multiarrow) |\eta| which satisfy |\varphi(\eta) = id| and |\varphi(f) \circ \eta = f| is equivalent to the natural isomorphism above.
To start translating this to rules, we look at |\eta| first. A direct translation would be to say we have the rule: $$\begin{align} \dfrac{}{a_1 : A_1, \dots, a_n : A_n \vdash \eta : A_1 \otimes \cdots \otimes A_n} \end{align}$$ This is unnatural because it treats |\eta| like a primitive open term. This also means that to use |\eta|, we’d need to use the Cut rule (which corresponds to substitution/composition) which would stymie Cut elimination. The solution is to mix a use of Cut into the rule itself producing the term |\eta[E_1/a_1, \dots, E_n/a_n]| which I’ll write more perspicuously as |E_1 \otimes \cdots \otimes E_n|. This gives rise to the rule: $$\begin{align} \dfrac{\Delta_1 \vdash E_1 : A_1 \quad \cdots \quad \Delta_n \vdash E_n : A_n}{\Delta_1,\dots,\Delta_n \vdash E_1 \otimes \cdots \otimes E_n : A_1 \otimes \cdots \otimes A_n}{\otimes_n}\text{I} \end{align}$$ Of course, we could restrict to just the |n=0| and |n=2| cases if we wanted. I’ll write the |n=0| case of |a_1\otimes\cdots\otimes a_n| as |*| in both the term and pattern cases. As the label for the rule, |\otimes_n I|, suggests, this is an introduction rule for |\otimes|.
The rule corresponding to |\varphi| takes less massaging. We’ll do the same trick of incorporating a Cut (Where?), but this makes a fairly minor difference in this case. The rule we get is: $$\begin{align} \dfrac{\Delta \vdash E : A_1 \otimes \cdots \otimes A_n \quad \Delta_l, a_1 : A_1, \dots, a_n : A_n, \Delta_r \vdash E' : B}{\Delta_l, \Delta, \Delta_r \vdash \mathsf{match}\ E\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ E' : B}{\otimes_n}\text{E},n \geq 1 \end{align}$$ Again, as the label suggests, this is an elimination rule for |\otimes|.
We then need equalities for the two equations and a third equality for naturality of |\varphi|. $$\begin{gather} \dfrac{\Delta_1 \vdash E_1 : A_1 \quad \cdots \quad \Delta_n \vdash E_n : A_n \quad \Delta_l, a_1 : A_1, \dots, a_n : A_n, \Delta_r \vdash E : B}{\Delta_l, \Delta_1, \dots, \Delta_n, \Delta_r \vdash (\mathsf{match}\ E_1\otimes\cdots\otimes E_n\ \mathsf{as}\ a_1\otimes\cdots\otimes a_n\ \mathsf{in}\ E) = E[E_1/a_1, \dots, E_n/a_n] : B}{\otimes}\beta \\ \\ \dfrac{\Delta \vdash E : A_1 \otimes \cdots \otimes A_n \quad \Delta_l, a : A_1 \otimes \cdots \otimes A_n, \Delta_r \vdash E' : B}{\Delta_l, \Delta, \Delta_r \vdash E'[E/a] = (\mathsf{match}\ E\ \mathsf{as}\ a_1\otimes\cdots\otimes a_n\ \mathsf{in}\ E'[(a_1\otimes\cdots\otimes a_n)/a]) : B}{\otimes}\eta \end{gather}$$ The first equation corresponds to an introduction immediately followed by an elimination which is the form of a |\beta|-rule. The second is an elimination followed by an introduction and gives rise to an |\eta|-rule.
Since we are considering a mapping-out property, the naturality equations gives rise to what is called a commuting conversion: $$\begin{align} \dfrac{\Delta \vdash E_1 : A_1 \otimes \cdots \otimes A_n \quad \Delta_l, a_1 : A_1, \dots, a_n : A_n, \Delta_r \vdash E_2 : B \quad b : B \vdash E_3 : C}{\Delta_l, \Delta, \Delta_r \vdash E_3[(\mathsf{match}\ E_1\ \mathsf{as}\ a_1 \otimes \dots \otimes a_n\ \mathsf{in}\ E_2)/b] = (\mathsf{match}\ E_1\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ E_3[E_2/b] : C}{\otimes}\text{CC} \end{align}$$
This rule is pretty bad from the perspective of structural proof theory. If I give you terms of the forms of the left and right hand sides of the equation, it can be quite difficult and potentially ambiguous to figure out what terms |E_2| and |E_3| should be. While this particular example can’t happen in our case, imagine if |E_3| did not use the variable |b|. This technically isn’t a problem for building a derivation or verifying it as you can just require that when someone invokes this rule they must specify what all the meta-variables are. Still, this causes difficulties for proof search and normalization and proofs of meta-theorems.
The solution is straightforward enough. We simply instantiate |E_3| with a concrete term. The not-so-straightforward part is knowing which terms we need. In this case, the main rule we need (and only one if we interpret the above as covering the |n = 0| case) is the following: $$\begin{align} \dfrac{\Delta \vdash E_1 : A_1 \otimes \cdots \otimes A_m \quad \Delta_l, a_1 : A_1, \dots, a_m : A_m, \Delta_r \vdash E_2 : B_1 \otimes \cdots \otimes B_n \quad \Delta_l', b_1 : B_1, \dots, b_n : B_n, \Delta_r' \vdash E_3 : C}{\begin{align}\Delta_l', \Delta_l, \Delta, \Delta_r, \Delta_r' \vdash &\ (\mathsf{match}\ (\mathsf{match}\ E_1\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_m\ \mathsf{in}\ E_2)\ \mathsf{as}\ b_1 \otimes \cdots \otimes b_n\ \mathsf{in}\ E_3) \\ = &\ (\mathsf{match}\ E_1\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ \mathsf{match}\ E_2\ \mathsf{as}\ b_1 \otimes \cdots \otimes b_m\ \mathsf{in}\ E_3) : C\end{align}}{\otimes}{\otimes}\text{CC} \end{align}$$
You can see that this rule presents no difficulty in picking out the subterms that should correspond to the meta-variables. Fortunately, we don’t need a rule for every possible top-level term the |E_3| from the first rule could be, let alone the infinite number of possible instantiations of |E_3|. Unfortunately, we do need one for each elimination rule, and so the number of commuting conversions grows roughly quadratically with the number of connectives.
The motivation for all these rules – the |\beta| and |\eta| rules as well as the commuting conversions – is ideally to have a well-defined normal form for terms that we can systematically reach. In particular, we want two terms to have the same normal form if and only if they are semantically equivalent. If we fail to have normal forms, we’d still at least want two terms to be in the same equivalence class induced by the equations if and only if they are semantically equivalent. Often, we only consider normal forms modulo the equivalence induced by commuting conversions and then endeavor to ensure that this equivalence is easily decidable.
If we were to consider a mapping-in property, e.g. |\mathcal C(\_, B) \times \mathcal C(\_, C) \cong \mathcal C(\_, B \times C)| for the categorical product, the story would be very similar except with introduction and elimination switched. We’d also find that we don’t need a commuting conversion rule, though we would need to expand any existing commuting conversions with the new eliminator. You can work through it and try to find where the naturality equation went.
See the appendix for a full and compact listing of the rules and an explicit formulation of what it means to interpret this language into a monoidal category.
Before we go on to examples of monoidal categories, let’s consider an example of a theory that we can formulate in our internal language. The main example is the theory of monoids. We assume a type |\mathsf M| and operations |\mathsf e : () \to \mathsf M| and |\mathsf m : (\mathsf M, \mathsf M) \to \mathsf M|. To this we add the equations, |\mathsf m(\mathsf e(), a) = a = \mathsf m(a, \mathsf e())| and |\mathsf m(\mathsf m(a_1, a_2), a_3) = \mathsf m(a_1, \mathsf m(a_2, a_3))|. As we can readily verify, all these equations use the free variables in order and exactly once on each side of the equations. You can contrast this to the axioms of a group and see that those axioms aren’t valid in our internal language. A model of the theory of a monoid in a monoidal category is known as a monoid object. Another theory we could formulate in our internal language is the theory of a monoid action.
For mathematicians, the archetypal example of a monoidal category is the category of vector spaces over a field |k|, e.g. the real numbers. The monoidal product is the tensor product of vector spaces with unit |k|. The multiarrows of the associated multicategory are multilinear maps. The tensor product is symmetric which corresponds to adding the structural rule of Exchange to our list of rules. In practice, this means while we’re still required to use each variable in the context of a term exactly once, we are no longer required to use them in order. A model of the theory of monoids in this monoidal category, i.e. a monoid object in this monoidal category, is exactly an associative, unital |k|-algebra. Closely related, a ring is exactly a monoid object in the monoidal category of abelian groups.
Another major class of monoidal categories is cartesian monoidal categories where the monoidal product is the categorical product. The category of vector spaces has categorical products so it forms a monoidal category with that as well. Therefore part of the data of a monoidal category is a specific choice of monoidal product as there can easily be many inequivalent monoidal products. In terms of our internal language, a cartesian monoidal product corresponds to adding all the structural rules: Exchange, Weakening, and Contraction. This means that we are free to use variables however we like, i.e. we can use them in any order, ignore them, or use them multiple times. Usually, categorical products are presented in terms of a mapping-in property as I mentioned in the previous section. For a type theory, this leads to having tupling and projections. A good exercise would be to look up (or formulate) the rules for product types and show how the rules we’ve provided, in addition to the structural rules, allows us to define projections and show that the relevant equations are satisfied. A monoid object in |\mathbf{Set}| with respect to its cartesian monoidal product is exactly what we typically mean by a monoid.
A final example is the category of endofunctors on a given category which becomes a strict, non-symmetric monoidal category with composition as the monoidal product and the identity functor as the unit. Our internal language then provides a rather different perspective on natural transformations. A natural transformation |\tau : F \circ G \to H| is now viewed as a binary operation |\tau : (F, G) \to H|. To be clear, this is still interpreted as a family of (unary) arrows |\tau_A : F(G(A)) \to H(A)|. The action on arrows (which are natural transformations in this case) of the monoidal product is horizontal composition of natural transformations. The famous example is, of course, the natural transformations |\mu : T \circ T \to T| and |\eta : Id \to T| become the operations |\mu : (T, T) \to T| and |\eta : () \to T| and the monad laws are exactly the monoid laws. That is, a monad is a monoid object in the category of endofunctors equipped with this monoidal product.
The category of endofunctors example is pretty nice, but it is weird to limit to just endofunctors. We can consider natural transformations from an arbitrary composable sequence of functors whose composite has the same source and target objects as the target functor. The source of this restriction is that our objects are (endo-)functors and the monoidal product needs to work on any pair of objects in any order. The solution to this is to use the fact that a monoidal category is exactly a one-object bicategory.
We can thus readily generalize to the internal language of a bicategory. As before, it was helpful to use the notion of a multicategory, at least in passing. The analogue of a multicategory in this context is a virtual bicategory. That is, a multicategory is to a monoidal category as a virtual bicategory is to a bicategory. Basically, a virtual bicategory is like a multicategory except that each object now has a specified source and target and instead of allowing arbitrary sequences as sources for multiarrows, we only allow composable sequences. Here, a composable sequence is a sequence of objects such that the target of one object in the sequence is the source of the next. The analogue of a representable multicategory is the existence of composites in our virtual bicategory. We can say a bicategory is a virtual bicategory that has all composites.
For our internal language, the only real change we need to make is to keep track of and enforce the composability constraint. One way of doing this is to modify our type formation judgement to |\vdash_S^T A| asserting that |A| is a linear type with source |S| and target |T|. Our typing judgement is similarly decorated producing |\Delta \vdash_S^T E : B|. |\Delta| is again of the form |a_1 : A_1, \dots, a_n : A_n|, but now there is the constraint that the source of |A_n| is |S|, the target of |A_1| is |T|, and the target of |A_i| is the source of |A_{i+1}| for |i < n|. This leads to rules like $$\begin{align} \dfrac{\Delta_1 \vdash_{T_1}^{T_0} E_1 : A_1 \quad \cdots \quad \Delta_n \vdash_{T_n}^{T_{n-1}} E_n : A_n}{\Delta_1,\dots,\Delta_n \vdash_{T_n}^{T_0} E_1 * \cdots * E_n : A_1 * \cdots * A_n} \end{align}$$ but nothing needs to change at the term level (though I did rename |\otimes| to |*| as that’s less misleading). The main (strict) bicategory would be |\mathbf{Cat}| where we’d interpret the linear types as functors and the linear terms as natural transformations.
Another direction for generalization is motivated by T-algebras where |T| is a monad. A |T|-algebra is an arrow |\alpha : TA \to A|. If we think of |\alpha| as a binary operation, |\alpha : (T, A) \to A|, similarly to how we viewed |\mu|, the |T|-algebra laws would look like |\alpha(\eta(), a) = a| and |\alpha(\mu(x, y), a) = \alpha(x, \alpha(y, a))|. These look exactly like the laws of a monoid action. The problem with this idea is that |T| and |A| are different kinds of objects; they live in different categories. One solution to this is to consider the internal language of an actegory.
An actegory is a monoidal category, |\mathcal C|, that acts on another category, |\mathcal D|. The quickest way of describing this is to say it is a strong monoidal functor from |\mathcal C \to [\mathcal D, \mathcal D]| where the (endo-)functor category |[\mathcal D, \mathcal D]| is equipped with composition as its monoidal product. We can uncurry this functor into a bifunctor |({-})\cdot({=}) : \mathcal C \times \mathcal D \to \mathcal D| satisfying |I\cdot D \cong D| and |(C \otimes C’)\cdot D \cong C \cdot (C’ \cdot D)|. For our |T|-algebras, |\mathcal C| would be |[\mathcal D, \mathcal D]|, and the monoidal functor would just be the identity.
To make the internal language, we’d start by including all the rules for a monoidal category to handle the structure on |\mathcal C|. Next, we’d add a judgement |\Delta / d : D \vdash E : D’| where |\Delta = c_1 : C_1, \dots, c_n : C_n|. This would have the same restriction that all variables, |c_1, \dots, c_n| and |d|, would need to be used exactly once and in the order they were written. The idea is that this would be interpreted as an arrow in |\mathcal D| from |(C_1 \otimes \cdots \otimes C_n)\cdot D \to D’|.
We’d have the rules (among others): $$\begin{gather} \dfrac{}{/ d : D \vdash d : D} \\ \\ \dfrac{\Delta \vdash E : C \quad \Delta' / d : D \vdash E' : D'}{\Delta, \Delta' / d : D \vdash E \cdot E' : C \cdot D'} \\ \\ \dfrac{\Delta / d : D \vdash E : C \cdot D' \quad c : C / d' : D' \vdash E' : D''}{\Delta / d : D \vdash \mathsf{match}\ E\ \mathsf{as}\ c \cdot d'\ \mathsf{in}\ E' : D''} \end{gather}$$
Presumably, you could formulate a notion of “virtual actegory” where the arrows consist of a list of objects from a multicategory |\mathcal C| and a final object from a category |\mathcal D| as their source and an object of |\mathcal D| as their target. You could imagine going further (or alternately) for an analogue of a (virtual) bicategory which would, again, amount to using composable sequences. (The name “biactegory” is already taken.)
Regardless, the above framework allows us to have |t : T / a : A \vdash \alpha(t, a) : A|, and we can then express our desired equations for a |T|-algebra in the form of the laws of a monoid action. One place where this notation comes in handy is in the connections between |T|-algebras and absolute colimits.
$$\begin{gather} \dfrac{\vdash A}{a : A \vdash a : A}\text{Ax} \qquad \dfrac{\Delta_1 \vdash E_1 : A_1 \quad \cdots \quad \Delta_n \vdash E_n : A_n \quad \Delta_l, a_1 : A_1, \dots, a_n : A_n, \Delta_r \vdash E: B}{\Delta_l, \Delta_1, \dots, \Delta_n, \Delta_r \vdash E[E_1/a_1,\dots,E_n/a_n] : B}\text{Cut} \\ \\ \dfrac{}{\vdash I}I\text{F} \qquad \dfrac{\vdash A_1 \quad \cdots \quad \vdash A_n}{\vdash A_1 \otimes \cdots \otimes A_n}{\otimes_n}\text{F}, n \geq 1 \qquad \dfrac{\mathsf A : \mathsf{Type}}{\vdash \mathsf A}\text{PrimType} \\ \\ \dfrac{\Delta_1 \vdash E_1 : A_1 \quad \cdots \quad \Delta_n \vdash E_n : A_n \quad \mathsf f : (A_1, \dots, A_n) \to B}{\Delta_1, \dots, \Delta_n \vdash \mathsf f(E_1, \dots, E_n) : B}\text{PrimTerm} \\ \\ \dfrac{}{\vdash * : I}I\text{I} \qquad \dfrac{\Delta_1 \vdash E_1 : A_1 \quad \cdots \quad \Delta_n \vdash E_n : A_n}{\Delta_1,\dots,\Delta_n \vdash E_1 \otimes \cdots \otimes E_n : A_1 \otimes \cdots \otimes A_n}{\otimes_n}\text{I} \\ \\ \dfrac{\Delta \vdash E : I \quad \Delta_l, \Delta_r \vdash E' : B}{\Delta_l, \Delta, \Delta_r \vdash \mathsf{match}\ E\ \mathsf{as}\ {*}\ \mathsf{in}\ E' : B}I\text{E} \qquad \dfrac{\Delta \vdash E : A_1 \otimes \cdots \otimes A_n \quad \Delta_l, a_1 : A_1, \dots, a_n : A_n, \Delta_r \vdash E' : B}{\Delta_l, \Delta, \Delta_r \vdash \mathsf{match}\ E\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ E' : B}{\otimes_n}\text{E},n \geq 1 \end{gather}$$
$$\begin{gather} \dfrac{\Delta \vdash E : B}{\Delta \vdash (\mathsf{match}\ {*}\ \mathsf{as}\ {*}\ \mathsf{in}\ E) = E : B}{*}\beta \qquad \dfrac{\Delta \vdash E : I \quad \Delta_l, a : I, \Delta_r \vdash E' : B}{\Delta_l, \Delta, \Delta_r \vdash E'[E/a] = (\mathsf{match}\ E\ \mathsf{as}\ {*}\ \mathsf{in}\ E'[*/a]) : B}{*}\eta \\ \\ \dfrac{\Delta_1 \vdash E_1 : A_1 \quad \cdots \quad \Delta_n \vdash E_n : A_n \quad \Delta_l, a_1 : A_1, \dots, a_n : A_n, \Delta_r \vdash E : B}{\Delta_l, \Delta_1, \dots, \Delta_n, \Delta_r \vdash (\mathsf{match}\ E_1\otimes\cdots\otimes E_n\ \mathsf{as}\ a_1\otimes\cdots\otimes a_n\ \mathsf{in}\ E) = E[E_1/a_1, \dots, E_n/a_n] : B}{\otimes_n}\beta \\ \\ \dfrac{\Delta \vdash E : A_1 \otimes \cdots \otimes A_n \quad \Delta_l, a : A_1 \otimes \cdots \otimes A_n, \Delta_r \vdash E' : B}{\Delta_l, \Delta, \Delta_r \vdash E'[E/a] = (\mathsf{match}\ E\ \mathsf{as}\ a_1\otimes\cdots\otimes a_n\ \mathsf{in}\ E'[(a_1\otimes\cdots\otimes a_n)/a]) : B}{\otimes_n}\eta \\ \\ \dfrac{\Delta \vdash E_1 : I \quad \Delta_l, \Delta_r \vdash E_2 : I \quad \Delta_l', \Delta_r' \vdash E_3 : C}{\Delta_l', \Delta_l, \Delta, \Delta_r, \Delta_r' \vdash (\mathsf{match}\ (\mathsf{match}\ E_1\ \mathsf{as}\ {*}\ \mathsf{in}\ E_2)\ \mathsf{as}\ {*}\ \mathsf{in}\ E_3) = (\mathsf{match}\ E_1\ \mathsf{as}\ {*}\ \mathsf{in}\ \mathsf{match}\ E_2\ \mathsf{as}\ {*}\ \mathsf{in}\ E_3) : C}{*}{*}\text{CC} \\ \\ \dfrac{\Delta \vdash E_1 : A_1 \otimes \cdots \otimes A_n \quad \Delta_l, a_1 : A_1, \dots, a_n : A_n, \Delta_r \vdash E_2 : I\quad \Delta_l', \Delta_r' \vdash E_3 : C}{\begin{align}\Delta_l', \Delta_l, \Delta, \Delta_r, \Delta_r' \vdash &\ (\mathsf{match}\ (\mathsf{match}\ E_1\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ E_2)\ \mathsf{as}\ {*}\ \mathsf{in}\ E_3) \\ = &\ (\mathsf{match}\ E_1\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ \mathsf{match}\ E_2\ \mathsf{as}\ {*}\ \mathsf{in}\ E_3) : C\end{align}}{\otimes_n}{*}\text{CC} \\ \\ \dfrac{\Delta \vdash E_1 : I \quad \Delta_l, \Delta_r \vdash E_2 : B_1 \otimes \cdots \otimes B_m \quad \Delta_l', b_1 : B_1, \dots, b_m : B_m, \Delta_r' \vdash E_3 : C}{\begin{align}\Delta_l', \Delta_l, \Delta, \Delta_r, \Delta_r' \vdash &\ (\mathsf{match}\ (\mathsf{match}\ E_1\ \mathsf{as}\ {*}\ \mathsf{in}\ E_2)\ \mathsf{as}\ b_1 \otimes \cdots \otimes b_m\ \mathsf{in}\ E_3) \\ = &\ (\mathsf{match}\ E_1\ \mathsf{as}\ {*}\ \mathsf{in}\ \mathsf{match}\ E_2\ \mathsf{as}\ b_1 \otimes \cdots \otimes b_m\ \mathsf{in}\ E_3) : C\end{align}}{*}{\otimes_m}\text{CC} \\ \\ \dfrac{\Delta \vdash E_1 : A_1 \otimes \cdots \otimes A_n \quad \Delta_l, a_1 : A_1, \dots, a_n : A_n, \Delta_r \vdash E_2 : B_1 \otimes \cdots \otimes B_m \quad \Delta_l', b_1 : B_1, \dots, b_m : B_m, \Delta_r' \vdash E_3 : C}{\begin{align}\Delta_l', \Delta_l, \Delta, \Delta_r, \Delta_r' \vdash &\ (\mathsf{match}\ (\mathsf{match}\ E_1\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ E_2)\ \mathsf{as}\ b_1 \otimes \cdots \otimes b_m\ \mathsf{in}\ E_3) \\ = &\ (\mathsf{match}\ E_1\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ \mathsf{match}\ E_2\ \mathsf{as}\ b_1 \otimes \cdots \otimes b_m\ \mathsf{in}\ E_3) : C\end{align}}{\otimes_n}{\otimes_m}\text{CC} \end{gather}$$
|\mathsf A : \mathsf{Type}| means that |\mathsf A| is a primitive type in the signature. |\mathsf f : (A_1, \dots, A_n) \to B| means that |\mathsf f| is assigned this type in the signature.
I did not write them, but the usual laws for equality (reflexivity and indiscernability of identicals) should be included.
A theory in this language is free to introduce additional linear types and linear operations.
Write |\den{-}| for the (overloaded) interpretation function. Its value on primitive operations is left as a parameter.
Associators for the semantic |\otimes| will be omitted below. We can arbitrarily assume a particular association of monoidal products and then the relevant associators are completely determined by the input and output types. There are multiple possible expressions for those associators, but the coherence conditions of monoidal categories guarantee that they are equal.
$$\begin{align} \vdash A \implies & \den{A} \in \mathsf{Ob}(\V) \\ \\ \den{\Delta} =\, & \den{A_1}\otimes \cdots \otimes \den{A_n} \text{ where } \Delta = a_1 : A_1, \dots, a_n : A_n \\ \den{I} =\, & I \\ \den{A_1 \otimes \cdots \otimes A_n} =\, & \den{A_1}\otimes \cdots \otimes \den{A_n} \\ \end{align}$$
$$\begin{align} \Delta \vdash E : A \implies & \den{E} \in \V(\den{\Delta}, \den{A}) \\ \\ \den{a} =\, & id_{\den{A}} \text{ where } a : A \\ \den{*} =\, & id_I \\ \den{E_1 \otimes \cdots \otimes E_n} =\, & \den{E_1} \otimes \cdots \otimes \den{E_n} \text{ where }\Delta_i \vdash E_i : A_i \\ \den{\mathsf{match}\ E\ \mathsf{as}\ {*}\ \mathsf{in}\ E'} =\, & \den{E'} \circ (id_{\den{\Delta_l}} \otimes (\lambda_{\den{\Delta_r}} \circ (\den{E} \otimes id_{\den{\Delta_r}}))) \\ \den{\mathsf{match}\ E\ \mathsf{as}\ a_1 \otimes \cdots \otimes a_n\ \mathsf{in}\ E'} =\, & \den{E'} \circ (id_{\den{\Delta_l}} \otimes \den{E} \otimes id_{\den{\Delta_r}}) \\ \den{\mathsf f(E_1, \dots, E_n)} =\, & \den{\mathsf f} \circ (\den{E_1} \otimes \cdots \otimes \den{E_n}) \text{ where }\mathsf f\text{ is an appropriately typed linear operation} \end{align}$$
where |\lambda_B : I \otimes B \cong B| is the left unitor.