simple.tex

\chapter{Simple type theories}
\label{chap:simple}

At this point we have done about all we can with \emph{unary} type theories, where the antecedent and consequent of each sequent consist only of a single type.
(In fact, most introductions to type theory skip over the unary case altogether, but I find it clarifying to start with cases that are as simple as possible.)
The most common type theories allow finite \emph{lists} of types as the antecedent.
These are the object of study in this chapter; we call them \emph{simple type theories}.
This term is more common in the literature than ``unary'', but perhaps not with the exact meaning we are giving it; the word ``simple'' is primarily used to contrast with ``dependent'' type theories (see \cref{chap:dtt}).


\section{Towards multicategories}
\label{sec:why-multicats}

As motivation for the generalization away from unary type theories, we consider a few problems with unary type theory, from a categorical perspective, that all turn out to have this as their solution.
Let's begin by stating some general principles of type theory.
Looking back at the rules of all our type theories, we see that they can be divided into two groups.
On the one hand, there are rules that don't refer specifically to any operation, such as the identity rule $x:X \types x:X$ and the cut rule.
On the other hand, there are rules that introduce or eliminate a particular operation on types, such as product, coproduct, and so on --- and each such rule refers to only \emph{one} operation  (such as $\times,+,f^*$, etc.).

This ``independence'' between the rules for distinct operations is important for the good behavior of type theory.
Many of the exercises have involved combining the rules for multiple previously-studied operations, and in \cref{sec:modularity} we remarked on how such operations tend to coexist ``without interacting'' in the metatheory: e.g.\
when proving the cut-admissibility theorems we essentially just commute the rules for different operations past each other.
This ``modularity'' means that we are always free to add new structure to a theory without spoiling the structure we already had.
We formulate it as a general principle:
\begin{equation}\label{princ:independence}
  \text{Each rule in a type theory should refer to only one operation}.\tag{$\ast$}
\end{equation}
(Like any general principle,~\eqref{princ:independence} is not always strictly adhered to.
For instance, we haven't discussed the $\equiv$ relation that have to be imposed on sequent calculus derivations to present non-posetal free categories, but these turn out to involve ``commutativity'' relations between \emph{different} type operations.
This is arguably another advantage of natural deduction.)

Note that despite~\eqref{princ:independence}, we can often obtain nontrivial results about the interaction of operations.
For instance, in \cref{ex:mslat-monoid} you showed that $A\meet \top\cong A$, even though $\meet$ and $\top$ are distinct operations with apparently unrelated rules.
Similarly, in \cref{ex:mslat-fib,ex:catprod-fib} you showed that $f^*$ preserves $\meet$ and $\times$.
In general, this tends to happen when relating operations whose universal properties all have the same ``handedness''.
For instance, all the operations $\meet,\top,\times,\unit,f^*$ have ``mapping in'' or ``from the right'' universal properties.
Thus, we can expect to compare two objects built using more than one of them by showing that they have the same universal property, and this is essentially what type theory does.

We also observed in \cref{sec:modularity} that in all cases we were able to extract the rules for a given operation from the universal property of the objects it was intended to represent in category theory.
The left and right rules in a sequent calculus, or the introduction and elimination rules in a natural deduction, always expressed the ``two sides'' of a universal property: one of them ``structures the object'' and the other says that it is universal with this structure.
The ``principal case'' of cut admissibility for a sequent calculus, and the $\beta$-conversion equality rule for a natural deduction, both express the fact that morphisms defined by the universal property ``compose with the structure'' to the inputs, e.g.\ a map $X\to A\times B$ defined from $f:X\to A$ and $g:X\to B$ gives back $f$ and $g$ when composed with the product projections.
Similarly, the proof of identity admissibility for a sequent calculus, and the $\eta$-conversion rule for a natural deduction, express the uniqueness half of the universal property.
This leads us to formulate another general principle:
\begin{equation}\label{princ:ump}
  \parbox{3.5in}{\centering The operations in a type theory should correspond categorically to objects with universal properties.}\tag{$\dagger$}
\end{equation}

The point is that from the perspective of unary type theory, these two principles \emph{seem} overly restrictive.
For instance, we remarked above that by expressing universal properties in type theory we can compare operations whose universal properties have the same handedness; but often we are interested in categorical structures satisfying nontrivial relations between objects with universal properties of different handedness.
For instance, in any category with both products and coproducts, there is a canonical map $(A\times B)+(A\times C) \to A\times (B+C)$, and the category is said to be \emph{distributive} if this map is always an isomorphism.
(When the category is a poset, we call it a \emph{distributive lattice}.)
However, we saw in \cref{sec:modularity} that if we simply combine the unary type theoretic rules for $\times$ and $+$, we get a type theory for categories with products and coproducts, but no interaction between them.
So unary type theory cannot deal with distributive categories while adhering to~\eqref{princ:independence} and~\eqref{princ:ump}.

Perhaps surprisingly, there \emph{is} a way to present a type theory for distributive categories.
The idea is to move into a world where the product $A\times B$ \emph{also} has a ``mapping out'' universal property, so that we can compare $(A\times B)+(A\times C)$ and $A\times (B+C)$ by saying they have the same universal property.
As we will see, this requires moving to a type theory with multiple antecedents.

This is one motivation.
Another is that we might want to talk about operations whose universal property can't be expressed in unary type theory while adhering to~\eqref{princ:independence}.
For instance, a \emph{cartesian closed category} has exponential objects such that morphisms $X\to Z^Y$ correspond to morphisms $X\times Y\to Z$; but how can we express this without referring to $\times$?
It turns out that the solution is the same.

We might also want to talk about operations that \emph{have} no obvious universal property, obviously violating~\eqref{princ:ump}.
For instance, what about monoidal categories?
In the usual presentation of a monoidal category, the tensor product $A\tensor B$ has no universal property.
It turns out that there is a way to give it a universal property, and this also leads us to higher-ary antecedents.

% Finally, there is also another motivation not having anything to do with~\eqref{princ:independence} and~\eqref{princ:ump}: we may want to generalize the ``input data'' \cG from which we generate our free objects.
% The unary type theory for categories with products allows us to prove theorems of the form ``in any category with products, for any morphisms $f:A\to B$, $g:C\to D$ \dots'', but it doesn't permit these quantifications to include ``for any $f:A\times B\to C$''.
% This is because the type theory generates a free category-with-products from a directed graph \cG whose vertices and edges are the objects and morphisms we hypothesize; but there is no way to express $f:A\times B\to C$ as an edge of \cG, since \cG has no products of objects yet.
% This problem turns out to have the same solution as well.

So much for motivation.
As already mentioned, on the type-theoretic side what we will do in this chapter is allow multiple types in the antecedent of a judgment (but still, for now, only one type in the consequent); we call these \emph{simple type theories}.
In a simple type theory the antecedent is often called the \emph{context}.

On the categorical side, what we will study are \emph{multicategories} of various sorts.
An ordinary multicategory is like a category but whose morphisms can have any finite list of objects as their domain, say $f:(A_1,\dots,A_n) \to B$, with a straightforward composition law.
There are many possible variations on this definition: in a symmetric multicategory the finite lists can be permuted, in a cartesian multicategory we can add unrelated objects and collapse equal ones, and so on.
All of these categorical structures are known as \emph{generalized multicategories}.
There is an abstract theory of generalized multicategories~\cite{cs:multicats,hermida:coh-univ,leinster:higher-opds,burroni:t-cats} that includes these examples and many others, but (at least in the current version of this chapter) we will simply work with concrete examples.

Our approach to the semantics of simple type theory can be summed up in the following additional principle:
\begin{equation}\label{princ:structural}
  \parbox{4.3in}{\centering The shape of the context and the structural rules in a simple type theory should mirror the categorical structure of a generalized multicategory.}\tag{$\ddagger$}
\end{equation}
The \emph{structural rules} are the rules that don't refer to any operation on types, such as identity and cut.
(In this chapter we will meet other structural rules, such as exchange --- corresponding to permutation of domains in a symmetric multicategory -- and contraction and weakening --- corresponding to diagonals and projections in a cartesian multicategory.)
Principle~\eqref{princ:ump} then tells us that the \emph{non-structural} rules (which are sometimes called \emph{logical} rules) should all correspond to objects with universal properties in a generalized multicategory, and principle~\eqref{princ:independence} tells us that each non-structural rule should involve only \emph{one} such object.

In sum, we have the following table of correspondences:
\begin{center}
  \begin{tabular}{c|c}
    Type theory & Category theory\\\hline
    Structural rules & Generalized multicategory\\
    Logical rules & Independent universal properties
  \end{tabular}
\end{center}
Here by ``independent universal properties'' I mean that the universal property of each object can be defined on its own without reference to any other objects defined by universal properties (unlike, for instance, the exponential in a cartesian closed category).

We might formulate one further principle based on our experience in \cref{chap:unary}:
\begin{equation}\label{princ:adm}
  \parbox{4in}{\centering Insofar as possible, structural rules should\\ be admissible rather than primitive.}\tag{\S}
\end{equation}
It is not generally possible to make \emph{all} the structural rules admissible; for instance, we have seen that for sequent calculus we need a primitive identity rule at base types, while for natural deduction we need a primitive identity rule at all types.
However, in \cref{chap:unary} we were always able to make the substitution/cut/composition rule admissible rather than primitive.
That will continue to be the case in this chapter, and we will also strive for admissibility of the new structural rules we introduce (exchange, weakening, and contraction).

Note that together our four principles say that insofar as possible, the ``algebraic operations'' in a categorical structure (such as composition and identities in a category or multicategory, permutation of domains in a symmetric multicategory, and so on) are exactly what we do \emph{not} include as primitive rules in type theory!
To put this differently, recall from the end of \cref{sec:identifying-initial-objects} that the initiality theorems for type theory are about showing that two different categories have the same initial object; we might then say that the effect of the above principles is to ensure that these two categories are \emph{as different as possible}.
This may seem strange, but to paraphrase John Baez\footnote{``Every interesting equation is a lie.''~\cite{baez:why-ncats}}, a proof that two things are the same is more interesting (and more useful) the more different the two things appear to begin with.

Another way to say it is that in category theory we take the algebraic structure of a category as primitive, and use them to define and characterize objects with universal properties; whereas in type theory we take the universal properties as primitive and deduce that the algebraic structure is admissible.
Put this way, one might say that type theory is even more category-theoretic than category theory; for what is more category-theoretic than universal properties?

This all been very abstract, so I recommend the reader come back to this section again at the end of this chapter.
However, for completeness let me point out now that this general correspondence is particularly useful when designing new type theories and when looking for categorical semantics of existing type theories.
On one hand, any type theory that adheres to~\eqref{princ:independence} should have semantics in a kind of generalized multicategory that can be ``read off'' from the shape of its contexts and its structural rules.
On the other hand, to construct a type theory for a given categorical structure, we should seek to represent that structure as a generalized multicategory in which all the relevant objects have independent universal properties; then we can ``read off'' from the domains of morphisms in those multicategories the shape of the contexts and the structural rules of our desired type theory.

We will not attempt to make this correspondence precise in any general way, and in practice it has many tweaks and variations that would probably be exceptions to any putative general theorem; but it is a useful heuristic.


\section{Introduction to multicategories}
\label{sec:multicats-catth}

From a categorical point of view, a multicategory can be regarded as an answer to the question ``in what kind of structure does a tensor product have a universal property?''
The classical tensor product of vector spaces (or, more generally, modules over a commutative ring) does have a universal property: it is the target of a universal bilinear map.
That is, there is a function $m:V\times W \to V\tensor W$ that is bilinear (i.e.\ $m(x,-)$ and $m(-,y)$ are linear maps for all $x\in V$ and $y\in W$), and any other bilinear map $V\times W \to U$ factors uniquely through $m$ by a linear map $V\tensor W \to U$.
Put differently, $V\tensor W$ is a representing object for the functor $\mathrm{Bilin}(V,W;-) : \bVect \to \bSet$.

Of course, this property determines the tensor product up to isomorphism (though of course one still needs some more or less explicit construction to ensure that such a representing object exists).
However, unlike many universal properties, it is not quite sufficient on its own to show that the tensor product behaves as desired.
In particular, to show that the tensor product is associative, we would naturally like to show that $V\tensor (W\tensor U)$ and $(V\tensor W)\tensor U$ are both representing objects for the functor of \emph{trilinear} maps $\mathrm{Trilin}(V,W,U;-)$, and hence isomorphic.
But this is not an abstract consequence of the fact that each binary tensor product represents bilinear maps;
what we need is a sort of ``relative representability'' such as $\mathrm{Trilin}(V,W,U;-) \cong \mathrm{Bilin}(V\tensor W,U;-)$.

Finally, when we come to prove that these associativity isomorphisms satisfy the pentagon axiom of a monoidal category, we need analogous facts about quadrilinear maps, at which point it is clear that we should be talking about $n$-linear maps for a general $n$.
A multicategory is the categorical context in which to do this: in addition to ordinary morphisms like an ordinary category (e.g.\ linear maps) it also contains $n$-ary maps for all $n\in\dN$ (e.g.\ multilinear maps).

% \subsection{Multicategories and representability}
% \label{sec:multicat-repr}

Formally, just as a category is a directed graph with composition and identities, a multicategory is a \emph{multigraph} with composition and identities.

\begin{defn}\label{defn:multigraph}
  A \textbf{multigraph} \cG consists of a set $\cG_0$ of \emph{objects}, together with for every object $B$ and every finite list of objects $(A_1,\dots,A_n)$ a set of \emph{arrows} $\cG(A_1,\dots,A_n;B)$.
\end{defn}

Note that $n$ can be $0$.
We say that an arrow in $\cG(A_1,\dots,A_n;B)$ is \textbf{$n$-ary}; the special cases $n=0,1,2$ are \emph{nullary}, \emph{unary}, and \emph{binary}.

\begin{defn}
  A \textbf{multicategory} \cM is a multigraph together with the following structure and properties.
  \begin{itemize}
  \item For each object $A$, an identity arrow $\idfunc_A\in\cM(A;A)$.
  \item For any object $C$ and lists of objects $(B_1,\dots,B_m)$ and $(A_{i1},\dots,A_{in_i})$ for $1\le i\le m$, a composition operation
    \begin{align*}
      \cM(B_1,\dots,B_m;C) \times \prod_{i=1}^m \cM(A_{i1},\dots,A_{in_i};B_i) &\too \cM(A_{11},\dots,A_{mn_m};C)\\
      (g,(f_1,\dots,f_m)) &\mapsto g\circ (f_1,\dots,f_m)
    \end{align*}
    [TODO: Picture]
  \item For any $f\in\cM(A_1,\dots,A_n;B)$ we have
    \begin{mathpar}
      \idfunc_B \circ (f) = f\and
      f\circ (\idfunc_{A_1},\dots,\idfunc_{A_n}) = f.
    \end{mathpar}
  \item For any $h,g_i,f_{ij}$ we have
    \begin{mathpar}
      (h\circ (g_1,\dots,g_m))\circ (f_{11},\dots,f_{mn_m}) =
      h \circ (g_1\circ (f_{11},\dots,f_{1n_1}), \dots, g_m \circ (f_{m1},\dots,f_{mn_m}))
    \end{mathpar}
  \end{itemize}
\end{defn}

The objects and unary arrows in a multicategory form a category; indeed, a multicategory with only unary arrows is exactly a category.
Vector spaces and multilinear maps, as discussed above, are a good example to build intuition.

While the above definition is the most natural one from a certain categorical perspective, there is another equivalent way to define multicategories.
If in the ``multi-composition'' $g\circ (f_1,\dots,f_m)$ all the $f_j$'s for $j\neq i$ are identities, we write it as $g \circ_i f_i$.
We may also write it as $g\circ_{B_i} f_i$ if there is no danger of ambiguity (e.g.\ if none of the other $B_j$'s are equal to $B_i$).
Thus we have \textbf{one-place composition} operations
\begin{multline*}
  \circ_i : \cM(B_1,\dots,B_n;C) \times \cM(A_1,\dots,A_m;B_i) \\
  \too \cM(B_1,\dots,B_{i-1},A_1,\dots,A_m,B_{i+1},\dots,B_n;C)
\end{multline*}
that satisfy the following properties:
\begin{itemize}
\item $\idfunc_B \circ_1 f = f$ (since $\idfunc_B$ is unary, $\circ_1$ is the only possible composition here).
\item $f\circ_i \idfunc_{B_i} = f$ for any $i$.
\item If $h$ is $n$-ary, $g$ is $m$-ary, and $f$ is $k$-ary, then
  \[ (h \circ_i g) \circ_{j} f=
  \begin{cases}
    (h\circ_j f)\circ_{i+k-1} g &\quad \text{if } j < i\\
    h\circ_i (g\circ_{j-i+1} f) &\quad \text{if } i \le j < i+m\\
    (h\circ_{j-m+1} f)\circ_{i} g &\quad \text{if } j \ge i+m
  \end{cases}
  \]
  [TODO: Picture]
  We refer to the second of these equations as \emph{associativity}, and to the first and third as \emph{interchange}.
\end{itemize}
Conversely, given one-place composition operations satisfying these axioms, one may define
\[ g\circ (f_1,\dots,f_m) = (\cdots((g \circ_m f_m) \circ_{m-1} f_{m-1}) \cdots \circ_2 f_2) \circ_1 f_1 \]
to recover the original definition of multicategory.
The details can be worked out by the interested reader (\cref{ex:multicat-defns}) or looked up in a reference such as~\cite{leinster:higher-opds}.

With multicategories in hand, we can give an abstract version of the characterization of the tensor product of vector spaces using multilinear maps.

\begin{defn}\label{defn:multicat-tensor}
  Given objects $A_1,\dots,A_n$ in a multicategory \cM, a \textbf{tensor product} of them is an object $\bigtensor_i A_i$ with a morphism $\chi:(A_1,\dots,A_n) \to \bigtensor_i A_i$ such that all the maps $(-\circ_i \chi)$ are bijections
  \[ \cM(B_1,\dots,B_k,\textstyle\bigtensor_i A_i,C_1,\dots,C_m;D) \toiso \cM(B_1,\dots,B_k,A_1,\dots,A_n,C_1,\dots,C_m;D). \]
\end{defn}

When $n=2$ we write a binary tensor product as $A_1\tensor A_2$.
When $n=0$ we call a nullary tensor product a \textbf{unit object} and write it as $\one$.
When $n=1$ a unary tensor product is just an object isomorphic to $A$.

In keeping with the usual ``biased'' definition of monoidal category (which has a binary tensor product and a unit object, with all other tensors built out of those), we will say that a multicategory is \textbf{representable} if it is equipped with a chosen unit object and a chosen binary tensor product for every pair of objects.
Let $\bRepMCat$ denote the category of representable multicategories and functors that preserve the chosen tensor products strictly.

\begin{thm}\label{thm:multicat-repr}
  The category \bRepMCat is equivalent to the category \bMonCat of monoidal categories.
\end{thm}
\begin{proof}
  It is easy to show that $(A_1\tensor A_2)\tensor A_3$ and $A_1 \tensor (A_2\tensor A_3)$, if they both exist, are both a ternary tensor product $\bigtensor_{i=1}^3 A_i$, and hence canonically isomorphic.
  Similarly, $A\tensor \one$ and $\one\tensor A$ are unary tensor products, hence canonically isomorphic to $A$.
  The coherence axioms follow similarly; thus any representable multicategory gives rise to a monoidal category.

  Conversely, any monoidal category \cM has an underlying multicategory defined by $\cM(A_1,\dots,A_n;B) = \cM(\bigtensor_i A_i;B)$, where $\bigtensor_i A_i$ denotes some tensor product of the $A_i$'s such as $(\cdots((A_1\tensor A_2)\tensor A_3)\cdots )\tensor A_n$.
  The coherence theorem for monoidal categories implies that the resulting hom-sets $\cM(A_1,\dots,A_n;B)$ are independent, up to canonical isomorphism, of the choice of bracketing.
  We can similarly use the coherence theorem to define the composition of this multicategory, and to show that the given tensor product and unit make it representable.
  Finally, the constructions are clearly inverse up to natural isomorphism.
\end{proof}

There are other good references on multicategories, such as~\cite{hermida:multicats,leinster:higher-opds}.
We end this section by discussing limits and colimits in multicategories, which are a bit less well-known.

% \subsection{Limits and colimits in multicategories}
% \label{sec:lim-colim-multicat}

We say that an object $\unit$ of a multicategory is \textbf{terminal} if for any $A_1,\dots, A_n$ there is a unique morphism $(A_1,\dots, A_n)\to \unit$.
Similarly, a \textbf{binary product} of $A$ and $B$ in a multicategory is an object $A\times B$ with projections $A\times B \to A$ and $A\times B\to B$, composing with which yields bijections
\[ \cM(C_1,\dots,C_n;A\times B) \too \cM(C_1,\dots,C_n;A) \times \cM(C_1,\dots,C_n;B)\]
for any $C_1,\dots,C_n$.
We will say a multicategory \textbf{has products} if it has a specified terminal object and a specified binary product for each pair of objects.
The following is entirely straightforward.

\begin{thm}\label{thm:multicat-prod}
  A monoidal category has products (in the sense of \cref{sec:catprod}) if and only if its underlying multicategory has products, and this yields an equivalence of categories.\qed
\end{thm}

Colimits in a multicategory are a bit more subtle.
We define a \textbf{binary coproduct} in a multicategory \cM to be an object $A+B$ with injections $A\to A+B$ and $B\to A+B$ composing with which induces bijections
\begin{multline*}
  \cM(C_1,\dots,C_n,A+B,D_1,\dots,D_m;E) \toiso\\
  \cM(C_1,\dots,C_n,A,D_1,\dots,D_m;E) \times \cM(C_1,\dots,C_n,B,D_1,\dots,D_m;E).
\end{multline*}
for all $C_1,\dots,C_n$ and $D_1,\dots, D_m$ and $E$.
Similarly, an \textbf{initial object} is an object $\zero$ such that for any $C_1,\dots,C_n$ and $D_1,\dots, D_m$ and $E$, there is a unique morphism $(C_1,\dots,C_n,\zero,D_1,\dots,D_m)\to E$.
We say a multicategory \textbf{has coproducts} if it has a specified binary coproduct for each pair of objects and a specified initial object.

By a \textbf{distributive monoidal category}, we mean a monoidal category thath has coproducts (in the sense of \cref{sec:catcoprod}) and such that the canonical maps
\begin{mathpar}
(A\tensor B)+(A\tensor C)\to A\tensor(B+C)\and
(B\tensor A)+(C\tensor A)\to (B+C)\tensor A\and
\zero \to A\tensor \zero\and
\zero\to \zero\tensor A
\end{mathpar}
are isomorphisms.
(A \textbf{distributive category} is a distributive cartesian monoidal category.)

\begin{thm}\label{thm:multicat-coprod}
  A monoidal category is distributive if and only if its underlying representable multicategory has coproducts, and this yields an equivalence of categories.
\end{thm}
\begin{proof}
  If \cM is distributive, then by induction we have
  \[ \textstyle
  \Big((\bigotimes_i C_i)\tensor A \tensor (\bigotimes_j D_j)\Big) +
  \Big((\bigotimes_i C_i)\tensor B \tensor (\bigotimes_j D_j)\Big)
  \;\cong\;
  (\bigotimes_i C_i)\tensor (A+B) \tensor (\bigotimes_j D_j)
  \]
  and similarly
  \[ \zero \;\cong\; \textstyle (\bigotimes_i C_i)\tensor \zero \tensor (\bigotimes_j D_j).\]
  Since the morphisms in the underlying multicategory of \cM are maps out of iterated tensor products in \cM, these isomorphisms imply that the latter has coproducts.

  Conversely, if the underlying multicategory of \cM has coproducts, then taking $n=m=0$ in their universal property we see that the ordinary category \cM has coproducts.
  Moreover, the universal property with $n=1$ and $m=0$ applied to the composites
  \begin{mathpar}
    (C,A) \to C\tensor A \to (C\tensor A)+(C\tensor B)\and
    (C,B) \to C\tensor B \to (C\tensor A)+(C\tensor B)
  \end{mathpar}
  gives a map $(C,A+B) \to (C\tensor A)+(C\tensor B)$, and the universal property of $\tensor$ then yields a map
  \[C\tensor(A+B) \to (C\tensor A)+(C\tensor B). \]
  It is straightforward to show that this is an inverse to the canonical map that exists in any monoidal category with coproducts, and similarly in the other cases; thus \cM is distributive.
  Finally, one can check that these constructions are inverse.
\end{proof}


\subsection*{Exercises}

\begin{ex}\label{ex:multicat-defns}
  Prove that the definitions of multicategory in terms of multi-composition and one-place composition are equivalent, in the strong sense that they yield isomorphic categories of multicategories.
\end{ex}

\begin{ex}\label{ex:multicat-repr}
  Fill in the details in the proof of \cref{thm:multicat-repr}.
\end{ex}

\begin{ex}\label{ex:mcat-lax-func}
  Show that the category whose objects are representable multicategories but whose morphisms are \emph{arbitrary} functors of multicategories is equivalent to the category of monoidal categories and \emph{lax} monoidal functors.
\end{ex}

\begin{ex}\label{ex:mcat-strong-func}
  Show that the category of representable multicategories and functors that ``preserve tensor products'', in the sense that if $\chi:(A_1,\dots,A_n) \to \bigtensor_i A_i$ is a tensor product then $F(\chi)$ is also \emph{a} tensor product, is equivalent to the category of monoidal categories and \emph{strong} monoidal functors.
\end{ex}

\begin{ex}\label{ex:multicat-coprod}
  Fill in the details in the proof of \cref{thm:multicat-coprod}.
\end{ex}


\section{Multiposets and monoidal posets}
\label{sec:multiposets-monpos}

\subsection{Multiposets}
\label{sec:multiposets}

We begin our study of type theory for multicategories with the posetal case.
A \textbf{multiposet} is a multicategory in which each set $\cM(A_1,\dots,A_n;B)$ has at most one element.
We consider the adjunction between the category \bMPos of multiposets and the category \bRelMGr of \emph{relational multigraphs}, i.e.\ sets of objects equipped with an $n$-ary relation ``$(a_1,\dots,a_{n-1})\le b$'' for all integers $n\ge 1$.
We would like to construct the free multiposet on a relational multigraph \cG using a type theory.

Its objects, of course, will be those of \cG, so we do not yet need a type judgment.
We represent its relations using a judgment written
\[A_1,A_2,\dots,A_n \types B.\]
As is customary, we use capital Greek letters such as $\Gamma$ and $\Delta$ to stand for finite lists (possibly empty) of types; thus the above general judgment can also be written $\Gamma\types B$.
We write ``$\Gamma_1,\Gamma_2,\dots,\Gamma_n$'' for the concatenation of such lists, and we also write for instance ``$\Gamma,A,\Delta$'' to indicate a list containing the type $A$ somewhere the middle.

At the moment, the only rules for this judgment will be identities and those coming from \cG.
Based on the lessons we learned from unary type theory, we represent the latter in Yoneda-style.
\begin{mathpar}
  \inferrule{ }{A\types A}\and
  \inferrule{(A_1,\dots,A_n \le B)\in\cG \\ \Gamma_1\types A_1 \\ \dots \\ \Gamma_n \types A_n}{\Gamma_1,\dots,\Gamma_n\types B}
\end{mathpar}
We call this the \textbf{cut-free type theory for multiposets under \cG}.
Note that we use the ``multi-composition'' in Yoneda-ifying the relations in \cG; this is absolutely necessary for the admissibility of cut.
By contrast, it is traditional to formulate the cut rule itself in terms of the one-place compositions:

\begin{thm}\label{thm:multiposet-cutadm}
  In the cut-free type theory for multiposets under \cG, the following cut rule is admissible: if we have derivations of $\Gamma\types A$ and of $\Delta,A,\Psi\types B$, then we can construct a derivation of $\Delta,\Gamma,\Psi\types B$.
\end{thm}
\begin{proof}
  We induct on the derivation of $\Delta,A,\Psi\types B$.
  If it is the identity rule, then $A=B$ and $\Delta$ and $\Psi$ are empty, so our given derivation of $\Gamma\types A$ is all we need.
  Otherwise, it comes from some relation $A_1,\dots,A_n \le B$ in \cG, where we have derivations of $\Gamma_i \types A_i$.
  Since then $\Delta,A,\Psi = \Gamma_1,\dots,\Gamma_n$, there msut be an $i$ such that $\Gamma_i = \Gamma_i',A,\Gamma_i''$, while $\Delta = \Gamma_1,\dots,\Gamma_{i-1},\Gamma_i'$ and $\Psi = \Gamma_i'',\Gamma_{i+1},\dots,\Gamma_n$.
  Now by the inductive hypothesis, we can construct a derivation of $\Gamma_i',\Gamma,\Gamma_i''\types A_i$.
  Applying the rule for $A_1,\dots,A_n \le B$ again, with this derivation in place of the original $\Gamma_i \types A_i$, gives the desired result.
\end{proof}

However, we can also prove admissibility of ``multi-cut'' directly:

\begin{thm}\label{thm:multiposet-multicutadm}
  In the cut-free type theory for multiposets under \cG, the following multi-cut rule is admissible: if we have derivations of $\Psi_i\types A_i$ for $1\le i\le n$, and also $A_1,\dots,A_n \types B$, then we can construct a derivation of $\Psi_1,\dots,\Psi_n\types B$.
\end{thm}
\begin{proof}
  If $A_1,\dots,A_n \types B$ ends with the identity rule, then $n=1$ and $A_1=B$, whence $\Psi_1\types A_1$ is what we want.
  Otherwise, it comes from some relation $C_1,\dots,C_m \le B$, where we have a partition $A_1,\dots,A_n = \Gamma_1,\dots,\Gamma_m$ and derivations of $\Gamma_j \types C_j$.
  Let $\Phi_j$ be the concatenation of all the $\Psi_i$ such that $A_i \in \Gamma_j$; then by the inductive hypothesis we can get $\Phi_j\types C_j$.
  Applying the generator rule again, we get $\Phi_1,\dots,\Phi_m \types B$, which is the desired result.
\end{proof}

The notation is certainly a bit heavier when constructing multi-cuts directly.
However, as we will see later on, in more complicated situations there are definite advantages to the latter.

\begin{thm}\label{thm:multiposet-initial}
  For any relational multigraph \cG, the free multiposet it generates has the same objects, and the relation $(A_1,\dots,A_n)\le B$ holds just when the sequent $A_1,\dots,A_n\types B$ is derivable in the cut-free type theory for multiposets under \cG.
\end{thm}
\begin{proof}
  \cref{thm:multiposet-cutadm}, together with the identity rule, tells us that this defines a multiposet $\F\bMPos\cG$.
  If $\cM$ is any other multiposet with a map $P:\cG\to\cM$ of relational multigraphs, then since the objects of $\F\bMPos\cG$ are those of \cG, there is at most one extension of $P$ to $\F\bMPos\cG$.
  It suffices to check that the relations in $\F\bMPos\cG$ hold in $\cM$; but this is clear since $\cM$ is a multiposet and the only rules are an identity and a particular multi-transitivity.
\end{proof}

Now we augment the type theory for multiposets with operations representing a tensor product.
Since the tensor product now has a universal property, this is essentially straightforward.
First of all, we need a type judgment $\types A\type$, with unsurprising rules:
\begin{mathpar}
  \inferrule{A\in\cG}{\types A\type}\and
  \inferrule{ }{\types \one\type}\and
  \inferrule{\types A\type \\ \types B\type}{\types A\tensor B\type}
\end{mathpar}

Second, in addition to the rules from \cref{sec:multiposets}, we have rules for $\tensor$.
Once again we need to make a choice between sequent calculus and natural deduction; we treat these one at a time.

\subsection{Sequent calculus for monoidal posets}
\label{sec:seqcalc-monpos}

The additional rules for the \textbf{sequent calculus for monoidal posets under \cG} are shown in \cref{fig:seqcalc-monpos}.
Since $A\tensor B$ has a ``mapping out'' universal property like a coproduct, the left rule expresses this universal property.
The right rule should be the universal relation $A,B\types A\tensor B$, but we have to Yoneda-ify it using the multicomposition.
The rules for $\one$ are similar.

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{\Gamma,A,B,\Delta\types C}{\Gamma,A\tensor B,\Delta\types C}\;\tensorL\and
    \inferrule{\Gamma\types A \\ \Delta\types B}{\Gamma,\Delta\types A\tensor B}\;\tensorR\and
    \inferrule{\Gamma,\Delta\types A}{\Gamma,\one,\Delta\types A}\;\one L\and
    \inferrule{ }{\types \one}\;\one R
  \end{mathpar}
  \caption{Sequent calculus for monoidal posets}
  \label{fig:seqcalc-monpos}
\end{figure}

Note the presence of the additional contexts $\Gamma$ and $\Delta$ in $\tensorL$ and $\one L$, which corresponds to the strong universal property of a tensor product in a multicategory referring to $n$-ary arrows for all $n$.

\begin{thm}\label{thm:monpos-identity}
  The general identity rule is admissible in the sequent calculus for monoidal posets under \cG: if $\types A\type$ is derivable, then so is $A\types A$.
\end{thm}
\begin{proof}
  By induction on the derivation of $\types A\type$.
  If $A\in \cG$, then $A\types A$ is an axiom.
  If $A=\one$, then $\one\types \one$ has the following derivation:
  \begin{mathpar}
    \inferrule*[Right=$\one L$]{\inferrule*[Right=$\one R$]{ }{\types \one}}{\one\types \one}
  \end{mathpar}
  And if $A=B\tensor C$, by the inductive hypothesis we have derivations $\sD_B$ and $\sD_C$ of $B\types B$ and $C\types C$, which we can put together like so:
  \begin{equation*}
    \inferrule*[Right=$\tensorL$]{
      \inferrule*[Right=$\tensorR$]{
        \inferrule*{\sD_B\\\\\vdots}{B\types B}\\
        \inferrule*{\sD_C\\\\\vdots}{C\types C}
      }{
        B,C\types B\tensor C
      }
    }{
      B\tensor C\types B\tensor C
    }\qedhere
  \end{equation*}
\end{proof}

The proof of cut-admissibility in this case has two new features we have not seen before.

\begin{thm}\label{thm:monpos-cutadm}
  Cut is admissible in the sequent calculus for monoidal posets under \cG: if we have derivations of $\Gamma\types A$ and of $\Delta,A,\Psi\types B$, then we can construct a derivation of $\Delta,\Gamma,\Psi\types B$.
\end{thm}
\begin{proof}
  % As always, we induct on the derivation of $\Delta,A,\Psi\types B$.
  If the derivation of $\Delta,A,\Psi\types B$ ends with the identity rule or a generating relation from \cG, we proceed just as in \cref{thm:multiposet-cutadm}.
  It cannot end with a $\one R$.
  If it ends with a $\tensorR$, we use the inductive hypotheses on its premises and apply $\tensorR$ again.

  The cases when it ends with a left rule introduce one new feature.
  Suppose it ends with a $\one L$.
  If $A$ is the $\one$ that was introduced by this rule, then we proceed basically as before: if $\Gamma\types A$ is $\one R$, so that $\Gamma$ is empty, then we are in the principal case and we can simply use the given derivation of $\Delta,\Psi\types B$; while if it is a left rule then we can apply a secondary induction.
  But it might also happen that $A$ is a different type, with the introduced $\one$ appearing in $\Delta$ or $\Psi$.
  However, this case is also easily dealt with by applying the inductive hypothesis to $\Gamma\types A$ and the given $\Delta,\Psi\types B$ (with $A$ appearing somewhere in its antecedents).
  In a direct argument for cut-elimination, we are transforming
  \begin{equation*}
    \inferrule*[right=cut]{
      \derivof{\Gamma\types A}\\
      \inferrule*[Right=$\one L$]{\derivof{\Delta_1,\Delta_2,A,\Psi\types B}}{\Delta_1,\one,\Delta_2,A,\Psi \types B}
    }{\Delta_1,\one,\Delta_2,\Gamma,\Psi\types B}
    \quad\leadsto\quad
    \inferrule*[right=$\one L$]{\inferrule*[Right=cut]{
      \derivof{\Gamma\types A}\\
      \derivof{\Delta_1,\Delta_2,A,\Psi\types B}
    }{\Delta_1,\Delta_2,\Gamma,\Psi\types B}}{\Delta_1,\one,\Delta_2,\Gamma,\Psi\types B}
  \end{equation*}

  The case when $\Delta,A,\Psi\types B$ ends with $\tensorL$ has a similar ``commutativity'' possibility.
  However, in this case there is also something new in the principal case, where $\Delta,A_1\tensor A_2,\Psi\types B$ is derived from $\Delta,A_1,A_2,\Psi\types B$, while $\Gamma\types A_1\tensor A_2$ is derived using $\tensorR$ from $\Gamma_1\types A_1$ and $\Gamma_2\types A_2$ (so that necessarily $\Gamma = \Gamma_1,\Gamma_2$).
  We would like to apply the inductive hypothesis twice to transform
  \begin{equation}\label{eq:monpos-cutam-1}
    \inferrule*[right=cut]{
      \inferrule*[right=$\tensorR$]{
        \derivof{\Gamma_1\types A_1}\\
        \derivof{\Gamma_2\types A_2}
      }{\Gamma_1,\Gamma_2\types A_1\tensor A_2}\\
      \inferrule*[Right=$\tensorL$]{
        \derivof{\Delta,A_1,A_2,\Psi\types B}
      }{\Delta,A_1\tensor A_2,\Psi\types B
      }}{\Delta,\Gamma_1,\Gamma_2,\Psi\types B}
  \end{equation}
  into
  \begin{equation}\label{eq:monpos-cutam-2}
    \inferrule*[Right=cut]{
      \derivof{\Gamma_2\types A_2}\\
      \inferrule*[Right=cut]{
        \derivof{\Gamma_1\types A_1}\\
        \derivof{\Delta,A_1,A_2,\Psi\types B}
      }{
        \Delta,\Gamma_1,A_2,\Psi\types B
      }
    }{
      \Delta,\Gamma_1,\Gamma_2,\Psi\types B
    }
  \end{equation}
  However, this is a problem for our usual style of induction.
  We can certainly apply the inductive hypothesis to $\Gamma_1\types A_1$ and $\Delta,A_1,A_2,\Psi\types B$ to get a derivation of $\Delta,\Gamma_1,A_2,\Psi\types B$.
  But this resulting derivation need not be ``smaller'' than our given derivation of $\Delta,A_1\tensor A_2,\Psi\types B$, so our inductive hypothesis does not apply to it.

  Probably the most common solution to this problem is to formulate the induction differently.
  Rather than inducting directly on the derivation of $\Delta,A,\Psi\types B$, we induct first on the type $A$ (the ``cut formula'')), and then do an ``inner'' induction on the derivation.
  All the ``commutativity'' cases do not change the cut formula, so there the inner inductive hypothesis continues to apply.
  But in the principal case for $\tensor$, both of the cuts we want to do inductively have smaller cut formulas than the one we started with ($A_1$ and $A_2$ versus $A_1\tensor A_2$), so they can be handled by the outer inductive hypothesis regardless of how large of derivations we need to apply them to.
\end{proof}

A different approach, however, is to prove the admissibility of multi-cut directly:

\begin{thm}\label{thm:monpos-multicutadm}
  Multi-cut is admissible in the sequent calculus for monoidal posets under \cG: if we have derivations of $\Psi_i\types A_i$ for $1\le i\le n$, and also $A_1,\dots,A_n \types B$, then we can construct a derivation of $\Psi_1,\dots,\Psi_n\types B$.
\end{thm}
\begin{proof}
  In this case we can return to inducting directly on the derivation of $A_1,\dots,A_n \types B$.
  The cases of identity and generator rules are just like in \cref{thm:multiposet-multicutadm}, and $\tensorR$ is just like the generator case.
  Unlike in \cref{thm:monpos-cutadm} it \emph{could} end with $\one R$, but in this case $n=0$ and there is nothing to be done.

  If it ends with $\one L$, then some $A_i = \one$, and we can forget about the corresponding $\Psi_i\types A_i$ and proceed inductively with the rest of them.
  (Note how even this case is simpler than in \cref{thm:monpos-cutadm}.)

  Finally, if it ends with $\tensorL$, then some $A_i = C\tensor D$, say, and we perform our secondary induction on $\Psi_i\types A_i$.
  Since $A_i=C\tensor D$ is not a base type, this derivation cannot end with the identity or generator rules, and of course it cannot end with $\one R$.
  If it ends with a left rule, we inductively cut with the premise of that rule and then apply it afterwards.
  The remaining case is when it ends with $\tensorR$, so that we have derivations of $\Gamma\types C$ and $\Delta\types D$ with $\Psi_i = \Gamma,\Delta$.
  But now we can inductively cut our given premise $A_1,\dots,A_{i-1},C,D,A_{i+1},\dots,A_n \types B$ with these two and also the given $\Psi_j\types A_j$ for $j\neq i$.
\end{proof}

That is, instead of transforming~\eqref{eq:monpos-cutam-1} into~\eqref{eq:monpos-cutam-2}, where we have to feed the output of one inductive cut into another inductive cut (which is what creates the problem), we transform
\begin{equation*}
  \inferrule*[right=cut]{
    \derivof{\Psi_j \types A_j} \\ % \;(A_j\neq C\tensor D)\\
    \inferrule*[right=$\tensorR$]{
      \derivof{\Gamma\types C}\\
      \derivof{\Gamma\types D}
    }{\Gamma,\Delta \types C\tensor D}\\
    \inferrule*[Right=$\tensorL$]{
      \derivof{A_1,\dots,C,D,\dots,A_n\types B}
    }{A_1,\dots,C\tensor D,\dots, A_n\types B
    }}{\Psi_1,\dots,\Gamma,\Delta,\dots,\Psi_n\types B}
\end{equation*}
into
\begin{equation*}
  \inferrule*[right=cut]{
    \derivof{\Psi_j \types A_j} \\ % \;(A_j\neq C\tensor D)\\
    \derivof{\Gamma\types C}\\
    \derivof{\Gamma\types D}\\
    \derivof{A_1,\dots,C,D,\dots,A_n\types B}
    }{\Psi_1,\dots,\Gamma,\Delta,\dots,\Psi_n\types B}
\end{equation*}
Thus, the multicategorical perspective leads to a simpler inductive proof of cut admissibility.
(Note, though, that to recover the one-place cut from the multi-cut requires composing with identities, hence invoking \cref{thm:monpos-identity} as well.)

In any case, we are ready to prove the initiality theorem, relating to an adjunction between the categoris \bRelMGr of relational multigraphs and \bMonPos of monoidal posets.
As always, the morphisms in our categories will be completely strict: so in particular the morphisms in \bMonPos are \emph{strict} monoidal functors.

\begin{thm}\label{thm:monpos-initial}
  For any relational multigraph \cG, the free monoidal poset generated by \cG is described by the sequent calculus for monoidal posets under \cG: its objects are the $A$ such that $\types A\type$ is derivable, while the relation $(A_1,\dots,A_n)\le B$ holds just when the sequent $A_1,\dots,A_n\types B$ is derivable.
\end{thm}
\begin{proof}
  As before, \cref{thm:monpos-identity,thm:monpos-cutadm} show that this defines a multiposet $\F\bMonPos\cG$.
  Moreover, the rules for $\tensor$ and $\one$ tell us that it is representable, hence monoidal.

  Now suppose $P:\cG\to\cM$ is a map into the underlying multiposet of any other monoidal poset.
  We can extend $P$ uniquely to a function from the objects of $\F\bMonPos\cG$ to those of $\cM$ preserving $\tensor$ and $\one$ on objects, so it remains to check that this is a map of multiposets and preserves the universal properties of $\tensor$ and $\one$.
  However, $\tensorR$ and $\one R$ are preserved by the universal data of $\tensor$ and $\one$ in \cM, while the universal properties of these data mean that $\tensorL$ and $\one L$ are also preserved.
\end{proof}

\subsection{Natural deduction for monoidal posets}
\label{sec:natded-monpos}

In natural deduction, the introduction rules $\tensorI$ and $\one I$ will coincide with the right rules $\tensorR$ and $\one R$ from the sequent calculus, but now we need elimination rules.
Since $\tensor$ and $\one$ in a multicategory have a ``mapping out'' universal property, these elimination rules will be reminiscent of the ``case analysis'' rules from \cref{sec:catcoprod}.
Formally speaking, they can be obtained by simply cutting $\tensorL$ and $\one L$ with an arbitrary sequent (thereby ``building in cuts'' to make the cut-admissiblity theorem easier).
\begin{mathpar}
  \inferrule*[Right=cut]{
    \Psi \types A\tensor B \\
    \inferrule*[Right=$\tensorL$]{\Gamma,A,B,\Delta\types C}{\Gamma,A\tensor B,\Delta\types C}
  }{
    \Gamma,\Psi,\Delta \types C
  }\and
  \inferrule*[Right=cut]{
    \Psi\types \one \\
    \inferrule*[Right=$\one L$]{\Gamma,\Delta\types A}{\Gamma,\one,\Delta\types A}
  }{
    \Gamma,\Psi,\Delta\types C
  }
\end{mathpar}
As usual in a natural deduction, we also need to assert the identity rule for all types.
Thus our complete \textbf{natural deduction for monoidal posets under \cG} consists of (the rules for $\types A\type$ and):
\begin{mathpar}
  \inferrule{\types A\type}{A\types A}\and
  \inferrule{(A_1,\dots,A_n \le B)\in\cG \\ \Gamma_1\types A_1 \\ \dots \\ \Gamma_n \types A_n}{\Gamma_1,\dots,\Gamma_n\types B}\and
  \inferrule{\Gamma\types A \\ \Delta\types B}{\Gamma,\Delta\types A\tensor B}\;\tensorI\and
  \inferrule{
    \Psi \types A\tensor B \\
    \Gamma,A,B,\Delta\types C
  }{
    \Gamma,\Psi,\Delta \types C
  }\;\tensorE\\
  \inferrule{ }{\ec\types \one}\;\one I\and
  \inferrule{
    \Psi\types \one \\
    \Gamma,\Delta\types C
  }{
    \Gamma,\Psi,\Delta\types C
  }\;\one E
\end{mathpar}

We leave the metatheory of this as an exercise (\cref{ex:natded-monpos}); it is also subsumed by the categorified version discussed in more detail in the next section.

\begin{rmk}\label{rmk:context-splitting-1}
  In \cref{sec:natded-mslat} we remarked that in (unary) natural deductions, the conclusions (bottoms) of rules always have an arbitrary type as antecedent (left side of $\types$).
  For simple type theories, the corresponding property is that the conclusions of rules should have an arbitrary \emph{context} on the left.
  This is not quite true for the above presentation of the rules, since most of their conclusions have an antecedent obtained by concatenating two or more contexts.
  However, such a rule is always equivalent to one whose conclusion involves an arbitrary context that is decomposed as a concatenation by an additional premise.
  For instance, the rule $\tensorI$ could equivalently be formulated as
  \begin{mathpar}
    \inferrule{\Psi = \Gamma,\Delta \\ \Gamma\types A \\ \Delta\types B}{\Psi\types A\tensor B}\;\tensorI\and
  \end{mathpar}
  while $\one I$ could be written
  \[ \inferrule{\Gamma=()}{\Gamma\types \one}\;\one I \]
  This is the appropriate point of view when reading rules ``bottom-up'' for type-checking or proof search, as discussed at the end of \cref{sec:rules}: to type-check or prove $\Psi\types A\tensor B$ we need to find an appropriate decomposition $\Psi = \Gamma,\Delta$ for which we can type-check or prove $\Gamma\types A$ and $\Delta\types B$.
  However, because this transformation is so straightforward, when writing informally one generally uses the simpler form with concatenated contexts in the conclusion.
\end{rmk}

\subsection*{Exercises}

\begin{ex}\label{ex:natded-monpos}
  Prove the well-formedness, cut-admissibility, and initiality theorems for the natural deduction for monoidal posets.
\end{ex}

\begin{ex}\label{ex:monpos-invertible}
  Prove that the rules $\tensorL$ and $\one L$ in the sequent calculus for monoidal posets are invertible in the sense of \cref{ex:mslat-invertible}: whenever we have a derivation of their conclusions, we also have derivations of their premises.
\end{ex}

\begin{ex}\label{ex:monpos-mslat}
  Write down either a sequent calculus or a natural deduction for monoidal posets that are also meet-semilattices, and prove its initiality theorem.
\end{ex}

\begin{ex}\label{ex:monpos-jslat}
  Let us augment the sequent calculus for monoidal posets by the following versions of the rules for join-semilattices:
  \begin{mathpar}
    \inferrule{\types A\type \\ \types B\type}{\types A\join B\type}\and
    \inferrule{ }{\types \bot\type}\and
    \inferrule{\Gamma \types A}{\Gamma\types A\join B}\and
    \inferrule{\Gamma \types B}{\Gamma\types A\join B}\and
    \inferrule{\Gamma,A,\Delta \types C\\\Gamma,B,\Delta \types C}{\Gamma,A\join B,\Delta\types C}\and
    \inferrule{ }{\Gamma,\bot,\Delta\types C}
  \end{mathpar}
  \begin{enumerate}
  \item Construct derivations in this calculus of the following sequents:
    \begin{align*}
      (A\tensor B)\join (A\tensor C) &\types  A\tensor (B\join C)\\
      A\tensor (B\join C) &\types (A\tensor B)\join (A\tensor C)
    \end{align*}
  \item Prove that this sequent calculus constructs the initial distributive monoidal poset (see \cref{thm:multicat-coprod}).
  \end{enumerate}
\end{ex}


\section{Multicategories and monoidal categories}
\label{sec:multicat-moncat}

Now we are ready to move back up from posets to categories; but here we encounter a bit of an expositional conundrum.
We have started with ordinary (non-symmetric, non-cartesian) multicategories since they are simpler from a category-theoretic perspective; in \cref{sec:cartmulti} we will introduce symmetric and cartesian multicategories by adding extra structure.
However, in type theory there are some ways in which the \emph{cartesian} case is the simplest.
This is essentially because our intuition tells us that ``variables can be used anywhere'', whereas in a non-cartesian type theory we have to control how many times a variable is used (and, in the non-symmetric case, what order they are used in).
Nevertheless we begin in this section (and the next) with a type theory for ordinary multicategories, as it introduces several important ideas that are clearer without the symmetric and cartesian structure to worry about; but we encourage the reader not to get too bogged down in details.


\subsection{Multicategories}
\label{sec:multicats}

Categorically, we begin with the adjunction between the category $\bMCat$ of multicategories and the category $\bMGr$ of multigraphs.
Let \cG be a multigraph; we augment the cut-free theory of \cref{sec:multiposets} with terms that represent the structure of derivations, as we did in \cref{sec:categories,sec:catprod,sec:catcoprod}.

Since our antecedents are now lists of formulas, we assign an abstract variable to \emph{each} of them, and we assign a single term involving these variables to the consequent.
Of course, we must assign distinct variables to distinct types in the list (or, more precisely, to distinct \emph{occurrences} of types, since the same type might occur more than once, and these occurrences should be assigned distinct variables).

Thus, for instance, we might have a judgment such as
\[ x:A, y:B, z:C \types f(x,g(y,z)):E \]
where $f\in\cG(A,D;E)$ and $g\in\cG(B,C;D)$.
Note that as always, the symbol $\types$ is the ``outermost''.
Moreover, the comma between abstract variable assignments binds more loosely than the typing colons; the above judgment should be read as
\[ ((x:A), (y:B), (z:C)) \types (f(x,g(y,z)):E). \]
As before, the derivation is actually determined by the term associated to the consequent \emph{together with} all the free variables in the context, which we can emphasize by writing
\[ xyz.f(x,g(y,z)) : (A, B, C \types E). \]

Since we now have multiple formal variables appearing in one sequent, it becomes important to keep track of which is which.
As in unary type theory, there are two ways to name variables.
In \textbf{de Bruijn style} we choose a fixed countably infinite set of variables, say $x_1,x_2,x_3,\dots$, and demand that any sequent with $n$ types in its context use the first $n$ of these variables \emph{in order}.
In fact there are two choices for this order; we might write
\[ x_1:A_1, x_2:A_2, \dots,x_n:A_n \types M:B \quad\text{or}\quad
x_n:A_n,\dots, x_2:A_2, x_1:A_1 \types M:B
\]
The first is called using \textbf{de Bruijn levels} and the second \textbf{de Bruijn indices}.

The second way to name variables is to allow arbitrary variables (perhaps taken from some fixed infinite set of variables), but keep track of $\alpha$-equivalence.
This now means that we can rename each variable independently, as long as we rename all of its occurrences at the same time and we don't try to rename any two variables to the same thing.
For instance, if $f\in\cG(A,A;B)$ then we can write four sequents
\[
\begin{array}{c@{\qquad}c}
  x:A, y:A \types f(x,y):B &
  x:A, y:A \types f(y,x):B \\\\
  y:A, x:A \types f(y,x):B &
  y:A, x:A \types f(x,y):B
\end{array}
\]
The two in the left column are the same by $\alpha$-equivalence, and similarly the two in the right column are identical; but the columns are distinct from each other.
(In fact, in the type theory of the present section, the sequents in the right-hand column are impossible; but in the theories to be considered in \cref{sec:stlc,sec:symmoncat} they will be possible.)

\begin{rmk}
The intent of $\alpha$-equivalence is that the names or labels of variables are themselves meaningless, but they carry the information of which variable occurrences in a term refer to which variables in the context (or, later, to which variable binding sites).
Bourbaki attempted to do away with variable labels entirely, writing all variable occurrences as $\Box$ and drawing connecting links to denote these references; thus the two columns above would be written
\[
\tikz[remember picture] \node[rectangle, inner sep=0pt] (a1) {$A$};,
\tikz[remember picture] \node[rectangle, inner sep=0pt] (a2) {$A$}; \types
f(\tikz[remember picture] \node[rectangle, inner sep=0pt] (b1) {$\Box$};,
\tikz[remember picture] \node[rectangle, inner sep=0pt] (b2) {$\Box$};) : B
\qquad
\tikz[remember picture] \node[rectangle, inner sep=0pt] (a1p) {$A$};,
\tikz[remember picture] \node[rectangle, inner sep=0pt] (a2p) {$A$}; \types
f(\tikz[remember picture] \node[rectangle, inner sep=0pt] (b2p) {$\Box$};,
\tikz[remember picture] \node[rectangle, inner sep=0pt] (b1p) {$\Box$};) : B
\]
\begin{tikzpicture}[remember picture,overlay]
  \draw (b2) -- +(0,-.6) -| (a2);
  \draw[white,ultra thick] (b1) -- +(0,-.4) -| (a1);
  \draw (b1) -- +(0,-.4) -| (a1);
  \draw (b2p) -- +(0,-.4) -| (a2p);
  \draw (b1p) -- +(0,-.6) -| (a1p);
\end{tikzpicture}

\noindent
However, this notation seems unlikely to catch on.
\end{rmk}

In \cref{sec:multiposets-monpos} we used capital Greek letters such as $\Gamma$ to denote finite lists of types.
As is also conventional, when we incorporate formal variables we use $\Gamma$ represent a finite list of types \emph{with variables attached} (with, of course, distinct variables attached to distinct occurrences of types), which is also called a \textbf{context}.
In general, $\Gamma$ represents ``the sort of thing that can go on the left of $\types$''.
%Thus, if $\Gamma = (x:A, y:B, z:C)$ then the above sequent would be $\Gamma\types f(x,g(y,z)):E$.

Now, the rules for multiposets and monoidal posets from \cref{sec:multiposets-monpos} involve, among other things, concatenation of such lists, which we wrote as $\Gamma,\Delta$.
But when $\Gamma$ and $\Delta$ contain variables, simple concatenation would not preserve the invariant that distinct occurrences of types are labeled by distinct variables, so something else must be going on.
If we use de Bruijn style, then the variable numbers in $\Gamma$ or $\Delta$ have to be incremented; we leave the details of this to the interested reader (\cref{ex:debruijn-context-concat}).
If we instead use arbitrary named variables, as we will generally do, then we simply need to apply $\alpha$-equivalences to $\Gamma$ and/or $\Delta$ to make their variable names disjoint.
(This is an instance of \cref{princ:term-der-alpha} that term notations for rules can require applying $\alpha$-equivalences to some premises for compatibility.
In \cref{sec:catprod} ``compatibility'' meant using the \emph{same} variable, while here it means using \emph{different} variables.)

From now on we will write simply $\Gamma,\Delta$ (and similarly $\Gamma, x:A, \Delta$, and so on) for the concatenation of two given contexts, modified to ensure variable distinctness in whatever way is appropriate.
Of course, any variable incrementing or $\alpha$-equivalence that happens in $\Gamma$ or $\Delta$ must also be applied to the consequents of any sequents they appear in.
On the other hand, if in some situation we \emph{assume} a sequent and write its context as $\Gamma,\Delta$, then no such operation is being applied; we are simply choosing a partition of that context into two parts.
When applying a rule ``top-down'', this applies to its premises, while when applying it ``bottom-up'', this applies to its conclusion (recall \cref{rmk:context-splitting-1}).

All this futzing around with variables may seem quite tedious and uninteresting.
It does matter in some situations; for instance, if mathematics is to be implemented in a computer, then all these technical issues must be dealt with carefully.
However, from our point of view these are all just different tricks to ensure that the terms with formal variables (modulo $\alpha$-equivalence) remain exact representations of derivation trees.
The terms where we have to rename variables and so on are only a \emph{notation} for the mathematical objects of real interest, namely derivations.
Remember this if you are ever in doubt about the meaning of variables or what sorts of renamings are possible.

With all of that out of the way, we can anticlimactically state the rules for the \textbf{cut-free type theory for multicategories under \cG}:
\begin{mathpar}
  \inferrule{A\in\cG}{x:A\types x:A}\and
  \inferrule{f\in \cG(A_1,\dots,A_n;B) \\ \Gamma_1\types M_1:A_1 \\ \dots \\ \Gamma_n \types M_n:A_n}{\Gamma_1,\dots,\Gamma_n\types f(M_1,\dots,M_n):B}\and
\end{mathpar}
We note that this theory has the following property.

\begin{lem}\label{thm:multicat-linear}
  If $\Gamma\types M:B$ is derivable, then every variable in $\Gamma$ appears exactly once in $M$.
\end{lem}
\begin{proof}
  By induction on the derivation.
  The identity rule $x:A\types x:A$ clearly has this property.
  And in the conclusion of the generator rule each variable appears in exactly one $\Gamma_i$, hence can only appear in one of the $M_i$'s, and by induction it appears exactly once there; hence it appears exactly once in $f(M_1,\dots,M_n)$.
\end{proof}

In type-theoretic lingo, \cref{thm:multicat-linear} says that our current type theory is \textbf{linear} (just like a linear polynomial uses each variable exactly once, a ``linear type theory'' uses each variable exactly once).
Note that linearity is a property of a system that we \emph{prove}, not a requirement that we impose from outside.
It is useful when proving that terms are derivations.

\begin{lem}\label{thm:multicat-tad}
  If $\Gamma\types N:B$ is derivable in the cut-free type theory for multicategories under \cG, then it has a unique derivation.
\end{lem}
\begin{proof}
  If $N=x$, then the derivation can only be $\idfunc$.
  And if $N=f(M_1,\dots,M_n)$, then by linearity each variable in $\Gamma$ must occur in exactly one of the subterms $M_1,\dots,M_n$.
  If $\Gamma\types N:B$ is derivable, then it must be that this partition of $\Gamma$ is ordered, $\Gamma=\Gamma_1,\dots,\Gamma_n$, and this (together with the known domain $(A_1,\dots,A_n)$ of $f$) determines the premises $\Gamma_i \types M_i:A_i$ that must be recursively checked (c.f.\ \cref{rmk:context-splitting-1})
\end{proof}

Linearity also has content as a statement about derivations rather than just their terms: it says that each occurrence of a type in the antecedent of a derivable sequent can be ``traced back up'' exactly one branch of the derivation tree.
For instance, in the following derivation
\begin{mathpar}
  \inferrule*{\inferrule*{ }{x:A\types x:A}\\
    \inferrule*{\inferrule*{ }{y:B\types y:B}\\
      \inferrule*{ }{z:A\types z:A
      }}{y:B,z:A \types g(y,z):X}\\
    \inferrule*{\inferrule*{ }{w:C\types w:C}}{w:C \types h(w):Y}
  }{x:A,y:B,z:A,w:C \types f(x,g(y,z),h(w)):Z}
\end{mathpar}
we can trace the occurrences of types in the antecedent of the conclusion as follows (omitting the variables and terms for brevity):
\begin{mathpar}
  \inferrule*{\inferrule*{ }{\tikz[remember picture] \node[red,rectangle,inner sep=0pt] (a2) {$A$};\types A}\\
    \inferrule*{\inferrule*{ }{\tikz[remember picture] \node[blue,rectangle,inner sep=0pt] (b3) {$B$};\types B}\\
      \inferrule*{ }{\tikz[remember picture] \node[green,rectangle,inner sep=0pt] (aa3) {$A$};\types A
      }}{\tikz[remember picture] \node[blue,rectangle,inner sep=0pt] (b2) {$B$};,
      \tikz[remember picture] \node[green,rectangle,inner sep=0pt] (aa2) {$A$}; \types X}\\
    \inferrule*{\inferrule*{ }{\tikz[remember picture] \node[purple,rectangle,inner sep=0pt] (c3) {$C$};\types C
      }}{\tikz[remember picture] \node[purple,rectangle,inner sep=0pt] (c2) {$C$}; \types Y}
  }{\tikz[remember picture] \node[red,rectangle,inner sep=0pt] (a1) {$A$};,
    \tikz[remember picture] \node[blue,rectangle,inner sep=0pt] (b1) {$B$};,
    \tikz[remember picture] \node[green,rectangle,inner sep=0pt] (aa1) {$A$};,
    \tikz[remember picture] \node[purple,rectangle,inner sep=0pt] (c1) {$C$};
    \types Z}
\begin{tikzpicture}[remember picture,overlay]
  \draw[->,red] (a1) -- (a2);
  \draw[->,blue] (b1) -- (b2); \draw[->,blue] (b2) -- (b3);
  \draw[->,green] (aa1) -- (aa2); \draw[->,green] (aa2) -- (aa3);
  \draw[->,purple] (c1) -- (c2); \draw[->,purple] (c2) -- (c3);
\end{tikzpicture}
\end{mathpar}

We now move on to the admissibility of cut/substitution.
For this we may again choose between the one-place cut and the multi-cut.
We choose the former, because the notation is less heavy, and because it matches the more common path taken in type theory.
(The advantage of multi-cut that we saw in \cref{sec:seqcalc-monpos} is not relevant for natural deduction, since there are no left rules.
We will see something analogous in \cref{sec:logic}, however.)
But we encourage the interested reader to write down a multi--substitution too (\cref{ex:moncat-multisubadm}).

\begin{thm}\label{thm:multicat-subadm}
  Substitution is admissible in the cut-free type theory for multicategories under \cG: given derivations of $\Gamma\types M:A$ and of $\Delta,x:A,\Psi\types N:B$, we can construct a derivation of $\Delta,\Gamma,\Psi\types M[N/x]:B$.
\end{thm}
\begin{proof}
  This is essentially just \cref{thm:multiposet-cutadm}, with terms carried along.
  There is one thing to be said: since the variables used in any context must be distinct, including the given context $\Delta,x:A,\Psi$, it must be that the variables in $\Delta$ and $\Psi$ are pairwise distinct, and all of them are distinct from $x$.
  But the variables in $\Delta,\Psi$ may not be pairwise distinct from those in $\Gamma$, so the context of the desired conclusion $\Delta,\Gamma,\Psi\types M[N/x]:B$ may involve an $\alpha$-equivalence.
  For instance, if we have $y:C\types f(y):A$ and $y:C,x:A,z:D\types g(y,x,z):B$, we cannot naively conclude $y:C,y:C,z:D\types g(y,f(y),z):B$; we have to rename one of the $y$'s first and get $y:C,w:C,z:D\types g(y,f(w),z):B$.
  We emphasize, however, that this is only a point about the term notation.
  The proof of \cref{thm:multiposet-cutadm}, which doesn't mention variables or terms at all, \emph{is already} an operation on derivations, and the renaming of variables only arises when we notate those derivations in a particular way.
\end{proof}

As before, note that we can regard this as defining substitution; its inductive clauses are
\begin{align*}
  x[M/x] &= M\\
  f(N_1,\dots,N_n)[M/x] &= f(N_1,\dots,N_{i-1},N_i[M/x],N_{i+1},\dots,N_n)
\end{align*}
where $i$ is the unique index such that $x$ occurs in $N_i$ (which exists by \cref{thm:multicat-linear}).

The one-place substitution operation defined in \cref{thm:multicat-subadm} will, of course, give the $\circ_i$ operations in our free multicategory.
The index $i$ is specified implicitly by the position of the variable $x$ in the context of $N$.
A similar thing happens with the associativity and interchange axioms.

\begin{thm}\label{thm:multicat-subassoc}
  Substitution in the cut-free type theory for multicategories satisfies the associativity/interchange rules:
  \begin{enumerate}
  \item If $\Gamma\types M:A$ and $\Delta,x:A,\Delta' \types N:B$ and $\Psi,y:B,\Psi'\types P:C$, then\label{item:multicat-subassoc-1}
    \[ P[N/y][M/x] = P[N[M/x]/y] \]
  \item If $\Gamma\types M:A$ and $\Delta \types N:B$ and $\Psi,x:A,\Psi',y:B,\Psi''\types P:C$, then\label{item:multicat-subassoc-2}
    \[ P[N/y][M/x] = P[M/x][N/y] \]
  \end{enumerate}
\end{thm}
\begin{proof}
  In both cases we induct on the derivation of $P$.
  For~\ref{item:multicat-subassoc-1}, if $P=y$ then both sides are $N[M/x]$.
  If $P=f(P_1,\dots,P_n)$, suppose $y$ occurs in $P_i$.
  Then $P[N/y] = f(P_1,\dots,P_i[N/y],\dots,P_n)$ and $x$ occurs in $P_i[N/y]$, so
  $P[N/y][M/x] = f(P_1,\dots,P_i[N/y][M/x],\dots,P_n)$ and the inductive hypothesis applies.

  For~\ref{item:multicat-subassoc-2}, we can't have $P$ being a single variable since there are two distinct variables in its context.
  Thus it must be $f(P_1,\dots,P_n)$, with $x$ and $y$ appearing in $P_i$ and $P_j$ respectively.
  If $i=j$, then we simply apply the inductive hypothesis to $P_i$; while if $i\neq j$ then
  \begin{equation*}
    P[N/y][M/x] = f(P_1,\dots,P_i[M/x],\dots,P_j[N/y],\dots,P_n) = P[M/x][N/y]\qedhere
  \end{equation*}
\end{proof}

If we used de Bruijn levels instead of arbitrary named variables, then the statement of \cref{thm:multicat-subassoc} would involve the same arithmetic on variable numbers that appears in the $\circ_i$ operations.
It is pleasing how the use of abstract variables eliminates this tedious bookkeeping.
(It is also possible to eliminate the bookkeeping at the multicategorical level by using an alternative definition of multicategories such as that of~\cite[Appendix A]{leinster:higher-opds}.)

\begin{thm}\label{thm:multicat-initial}
  For any multigraph \cG, the free multicategory generated by \cG can be described by the cut-free type theory for multicategories under \cG: its objects are those of \cG, and its morphisms $\Gamma\to B$ are the derivations of $\Gamma\types B$ (or equivalently, the derivable term judgments $\Gamma\types M:B$ modulo $\alpha$-equivalence).
\end{thm}
\begin{proof}
  \cref{thm:multicat-subadm} gives us the one-place composition operations, and \cref{thm:multicat-subassoc} verifies the associativity/interchange axiom for these.
  The two identity axioms are $x[M/x]=M$ (one of the defining clauses of substitution) and ``$M[y/x] = M$'', which looks false or nonsensical but is actually just an instance of $\alpha$-equivalence.

  Thus, we have a multicategory $\F\bMCat\cG$.
  Let \cM be any multicategory and $P:\cG\to\cM$ a map of multigraphs; as usual we extend $P$ to the morphisms of $\F\bMCat\cG$ by induction on derivations, and such an extension is forced since the rules are all instances of functoriality.
  Finally we verify by induction on derivations that this extension is in fact functorial on all composites.
\end{proof}


\subsection{Monoidal categories}
\label{sec:moncat}

We now extend the term notation of \cref{sec:multicats} to the natural deduction for monoidal posets from \cref{sec:natded-monpos}, obtaining a \textbf{simple type theory for monoidal categories under \cG} shown in \cref{fig:moncat}.

The rule $\tensorI$, like the rule $\timesI$ from \cref{sec:catprod}, ``pairs up'' two derivations of $\Gamma\types A$ and $\Delta\types B$, and thus must include terms notating both.
In this case, however, rather than pulling out the same variable from each, we require that the variables used are disjoint, so that we can concatenate the contexts in the conclusion.
Thus once again we are pairing up only the term parts (associated to the consequents), but the variables in the two contexts remain distinct; to emphasize this difference we use a different notation $\tpair M N$ instead of $\pair M N$.

The rule $\tensorE$, on the other hand, is more like the rule $\plusE$ from \cref{sec:catcoprod}: it has to include terms for both premises, one of which involves variables not appearing in the conclusion.
But unlike in \cref{sec:catcoprod}, the term $N$ can contain other variables that remain in the context of the conclusion (and must be disjoint from those in $M$, by $\alpha$-equivalence if necessary).
We only need to ``bind'' the other two variables $x$ and $y$.
Thus, for instance, the following application of $\tensorI$:
\begin{mathpar}
  \inferrule*{u:C, v:D \types \tpair{f(u)}{g(v)}:A\tensor B\\
  z:G,x:A,y:B,w:H \types h(z,x,y,w):K
  }{z:G,u:C,v:D,w:H\types \match_\tensor(\tpair{f(u)}{g(v)}, xy.h(z,x,y,w)):K}
\end{mathpar}
produces a term % $\match_\tensor(\tpair{f(u)}{g(v)}, xy.h(z,x,y,w))$
in which the variables $z,w$ in $h(z,x,y,w)$ are free, in addition to the free variables $u,v$ in $\tpair{f(u)}{g(v)}$.
% (This term is also a counterexample to a natural conjecture that the variables in a term must appear in the same order that they do in the context.)

Intuitively, because the tensor product has a ``mapping out'' universal property like a coproduct (that is, it is a ``positive type''), its elimination rule is a sort of ``case analysis'' that decomposes an element of $A\tensor B$ into an element of $A$ and an element of $B$, rather than a pair of projections.
Just as the rule $\plusE$ says that ``to do something with an element of $A+B$, it suffices to assume that it is either $\inl(u)$ or $\inr(v)$'', the rule $\tensorE$ says that ``to do something with an element of $A\tensor B$, it suffices to assume that it is $\tpair{x}{y}$.''
And just as the variables $u$ and $v$ are ``bound'' in the term syntax $\acase AB(M,u.P,v.Q)$ for coproducts, the variables $x$ and $y$ are bound in the term syntax $\match_{A\tensor B}^{\Gamma|\Delta}(M,xy.N)$.
The annotations $A\tensor B$ and $\Gamma|\Delta$ are to make type-checking possible (see \cref{thm:moncat-tad}); but generally we will omit them and write simply $\match_\tensor(M,xy.N)$.

The case of $\one$ is similar but simpler: to do something with an element of $\one$, it suffices to assume that it is $\ott$.
This gives no extra information, so no new variables are bound.
That is, the term syntax $\match_\one(M,N)$ binds nothing in $N$; it simply allows us to ignore $M$ (while keeping the free variables of $M$ in the context).

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{\types A\type}{x:A\types x:A}\and
    \inferrule{f\in \cG(A_1,\dots,A_n;B) \\ \Gamma_1\types M_1:A_1 \\ \dots \\ \Gamma_n \types M_n:A_n}{\Gamma_1,\dots,\Gamma_n\types f(M_1,\dots,M_n):B}\and
    \inferrule{\Gamma\types M:A \\ \Delta\types N:B}{\Gamma,\Delta\types \tpair{M}{N}:A\tensor B}\;\tensorI\and
    \inferrule{
      \Psi \types M:A\tensor B \\
      \Gamma,x:A,y:B,\Delta\types N:C
    }{
      \Gamma,\Psi,\Delta \types \match_{A\tensor B}^{\Gamma|\Delta}(M,xy.N):C
    }\;\tensorE\\
    \inferrule{ }{\ec\types \ott:\one}\;\one I\and
    \inferrule{
      \Psi\types M:\one \\
      \Gamma,\Delta\types N:C
    }{
      \Gamma,\Psi,\Delta\types \match_\one(M,N):C
    }\;\one E
  \end{mathpar}
  \caption{Simple type theory for monoidal categories}
  \label{fig:moncat}
\end{figure}

Like the theory of \cref{sec:multicats}, this theory is linear:

\begin{lem}\label{thm:moncat-linear}
  If $\Gamma\types M:B$ is derivable in the simple type theory for monoidal categories under \cG, then every variable in $\Gamma$ appears exactly once free in $M$.
\end{lem}
\begin{proof}
  By induction on the derivation.
  The cases of variables and generators are as in \cref{thm:multicat-linear}.
  For a pair $\tpair M N$ coming from $\tensorI$, each variable in $\Gamma,\Delta$ appears in exactly one of $\Gamma$ and $\Delta$, hence in exactly one of $M$ and $N$; we then apply the inductive hypotheses to $M$ or $N$ respectively.
  Similarly, for $\match_\tensor(M,xy.N)$ coming from $\tensorE$, each variable in $\Gamma,\Psi,\Delta$ must appear in exactly one of $\Gamma$, $\Psi$, or $\Delta$; by induction then in the first and third cases it must appear exactly once in $N$, and in the second case it must appear exactly once in $M$.
  The case of $\one E$ is similar, while there are no variables at all in $\ott$.
\end{proof}

\begin{lem}\label{thm:moncat-tad}
  If $\Gamma\types N:B$ is derivable in the simple type theory for monoidal categories under \cG, then it has a unique derivation.
\end{lem}
\begin{proof}
  The cases of $\idfunc$ and $f$ are as in \cref{thm:multicat-tad}, and the case of $\tensorI$ is similar, while $\one I$ is trivial.
  For $\match_\one(M,N)$, by linearity each variable occurs in exactly one of $M$ or $N$.
  If such a term is derivable, then the variables occurring in $M$ must be contiguous in the context, thereby splitting it as $\Gamma,\Psi,\Delta$ and determining the premises.
  If it should happen that \emph{no} variables occur in $M$ (such as if $M=\star$), then of course $\Psi=()$, but the splitting $\Gamma,\Delta$ is not uniquely determined; however since the premise has a re-joined context $\Gamma,\Delta$ anyway this doesn't matter.

  In the case of $\tensorE$, however, this latter point makes a difference, because the premise \emph{does} depend on which variables end up in $\Gamma$ and which in $\Delta$.
  This is why we have included the $\Gamma|\Delta$ annotation on $\match_\tensor^{\Gamma|\Delta}(M,xy.N)$, so that the context splitting is determined even if $M$ contains no variables.
  (See \cref{ex:moncat-context-splitting}.)
\end{proof}

\begin{lem}\label{thm:moncat-subadm}
  Substitution is admissible in the simple type theory for monoidal categories under \cG, in the same sense as \cref{thm:multicat-subadm}.
  Moreover, it is associative and interchanging in the same sense as \cref{thm:multicat-subassoc}.
\end{lem}
\begin{proof}
  The method is the same as that of \cref{thm:multiposet-cutadm}.
  Given judgments $\Gamma\types M:A$ and $\Delta,x:A,\Psi \types N:B$ (involving disjoint variables), we induct on the derivation of $N$.
  If the derivation is $\idfunc$, then $\Delta$ and $\Psi$ are empty and $N=x$, in which case we can just use $M$ itself.
  In all other cases, by \cref{thm:moncat-linear} the variable $x$ must appear in exactly one of the premises of the last rule applied to derive $N$ (which is to say, in exactly one of the subterms appearing in $N$ itself), and we inductively perform the substitution there.

  Explicitly, the defining clauses of the substitution operation are shown in \cref{fig:moncat-sub}.
%  (The case of $\ott$ actually does fit the general pattern discussed above, remembering that the rule $\one I$ has \emph{no} premises.)
  (Technically we also ought to indicate how the $\Gamma|\Delta$ superscripts on $\match_\tensor$ are frobnicated, but we leave that to the fastidious reader.)
  The proof of associativity and interchange is essentially the same as before: all the other rules behave just like the generator rules, except for $\ott$ where the claim is trivial.
\end{proof}

\begin{figure}
  \centering
  \begin{alignat*}{2}
    x[M/x] &= M\\
    f(N_1,\dots,N_n)[M/x] &= f(N_1,\dots,N_i[M/x],\dots,N_n) &&\quad\text{if $x$ occurs in $N_i$}\\
    \tpair P Q[M/x] &= \tpair{P[M/x]}{Q} &&\quad\text{if $x$ occurs in $P$}\\
    \tpair P Q[M/x] &= \tpair{P}{Q[M/x]} &&\quad\text{if $x$ occurs in $Q$}\\
    \match_\tensor(N,uv.P)[M/x] &= \match_\tensor(N[M/x],uv.P) &&\quad\text{if $x$ occurs in $N$}\\
    \match_\tensor(N,uv.P)[M/x] &= \match_\tensor(N,uv.P[M/x]) &&\quad\text{if $x$ occurs in $P$}\\
    % \match_\tensor^{\Gamma|\Delta}(N,uv.P)[M/x] &= \match_\tensor^{\Gamma|\Delta}(N[M/x],uv.P) &&\quad\text{if $x$ occurs in $N$}\\
    % \match_\tensor^{\Gamma_1,x,\Gamma_2|\Delta}(N,uv.P)[M/x] &= \match_\tensor^{\Gamma_1,\Psi,\Gamma_2|\Delta}(N,uv.P[M/x]) &&\quad\text{$\Psi$ the context of $M$}\\
    % \match_\tensor^{\Gamma|\Delta_1,x,\Delta_2}(N,uv.P)[M/x] &= \match_\tensor^{\Gamma|\Delta_1,\Psi,\Delta_2}(N,uv.P[M/x]) &&\quad\text{$\Psi$ the context of $M$}\\
    \ott[M/x] &&&\quad\text{cannot happen}\\
    \match_\one(N,P)[M/x] &= \match_\one(N[M/x],P) &&\quad\text{if $x$ occurs in $N$}\\
    \match_\one(N,P)[M/x] &= \match_\one(N,P[M/x]) &&\quad\text{if $x$ occurs in $P$}
  \end{alignat*}
  \caption{Substitution in the simple type theory for monoidal categories}
  \label{fig:moncat-sub}
\end{figure}

There is one final point to be made here about $\alpha$-equivalence: in the rule $\match_\tensor(N,uv.P)[M/x] = \match_\tensor(N,uv.P[M/x])$, we must rename variables to ensure that $u$ and $v$ do not appear free in $M$.
Otherwise, such a $u$ or $v$ in $M$ would after substitution be ``in the scope'' of the binding of $u$ or $v$, whereas all the free variables of $M$ ought to remain free in the substituted term.
(This issue didn't arise in \cref{sec:catcoprod} because there it was not possible to substitute into the subterms $u.P$ and $v.Q$ of a $\case$ term containing bound variables, since they could not contain any \emph{other} variables to be substituted for.)
When we regard substitution as an operation on derivations, the point is that to eliminate a cut after $\tensorE$ of the following sort:
\begin{mathpar}
  \inferrule*[Right=cut]{
    \Gamma\types M:A \\
    \inferrule*[Right=$\tensorE$]{
      \Xi \types N:C\tensor D\\
      \Delta_1,x:A,\Delta_2,u:C,v:D,\Psi \types P:B
    }{\Delta_1,x:A,\Delta_2,\Xi,\Psi \types \match_\tensor(N,uv.P):B
    }}{\Delta_1,\Gamma,\Delta_2,\Xi,\Psi \types \match_\tensor (N,uv.P[M/x]):B}
\end{mathpar}
we have to inductively cut
\begin{mathpar}
  \inferrule*[Right=cut]{
    \Gamma\types M:A \\
    \Delta_1,x:A,\Delta_2,u:C,v:D,\Psi \types P:B
  }{\Delta_1,\Gamma,\Delta_2,u:C,v:D,\Psi \types P[M/x]:B}
\end{mathpar}
and in order for \emph{this} cut to satisfy the variable condition explained in \cref{thm:multicat-subadm}, it must be that $u$ and $v$ do not occur in $\Gamma$.

When one takes terms with named variables as primary, this sort of ``capture-avoiding substitution'' is both necessary and tedious.
The de Bruijn methods avoid it, though at a fairly severe cost to readability.
But with substitution treated as an operation on derivations, there are no variables to ``capture'' and nothing to worry about.

With substitution in hand, we can state the $\beta$- and $\eta$-conversion rules that implement the universal properties.
\begin{mathpar}
  \match_\tensor(\tpair M N,xy.P) \equiv P[M/x,N/y]\and
  \match_\tensor(M,xy.N[\tpair xy/u]) \equiv N[M/u]\\
  \match_\one(\ott,N) \equiv N\and
  \match_\one(M,N[\ott/u]) \equiv N[M/u]
\end{mathpar}
As before, the $\beta$-conversion rule says that the map out of $A\tensor B$ defined by its universal property has the correct composite with the universal morphism $(A,B)\to A\tensor B$, while the $\eta$-conversion rule says that any map out of $A\tensor B$ is determined by the universal property from its composite with the universal morphism.
The rules for $\one$ are similar.

\begin{thm}\label{thm:moncat-initial}
  The free monoidal category generated by a multigraph \cG (or, more precisely, its underlying multicategory) can be described by the simple type theory for monoidal categories under \cG: its objects are the $A$ such that $\types A\type$, and its morphisms are the derivations of $\Gamma\types A$ (or the derivable judgments $\Gamma\types M:A$) modulo the congruence $\equiv$.
\end{thm}
\begin{proof}
  \cref{thm:moncat-subadm} shows that we obtain a multicategory $\F\bMonCat\cG$ this way, just as in \cref{thm:multicat-initial}.
  The rules for $\tensor$ and $\one$, together with the $\beta$- and $\eta$-rules for $\equiv$, tell us that it is representable, and hence a monoidal category.
  Now if \cM is a monoidal category and $P:\cG\to\cM$ a map of multigraphs, we extend it to $\F\bMonCat\cG$ by induction on derivations (of objects and morphisms and equalities) using the fact that \cM is a representable multicategory, observe that this definition is forced by functoriality and (strict) preservation of the monoidal structure, and then prove by induction that it is indeed a functor.
\end{proof}

Note that as in \cref{thm:catcoprod-initial}, we have to be careful to do the induction in the right order.
Since the rules for equalities refer to substitution, we have to first define the functor on types and terms, then prove that it maps substitution to composition, then define it on equalities.
This will be the case for almost all type theories we consider from now on (the case of products in \cref{sec:catprod} is very special in that its equality rules don't need to refer to substitution), so for the most part we will no longer bother to mention it.

\begin{rmk}\label{rmk:moncat-pres}
  In \cref{sec:unary-theories} we mentioned that every kind of type theory can be generalized to use an appropriate kind of ``presentation'' (or ``theory'') as input.
  This is true for all the type theories in the current chapter; but we postpone discussion of it for a while, because the notion of 1-skeleton for non-symmetric monoidal categories entails some technical complications that would significantly derail us at this point for very little benefit.
  We will mention presentations for the posetal case (where the problem of 1-skeletons doesn't arise) briefly in \cref{sec:logic}, and then start dealing with the 1-skeletons in the cartesian case (where they are simpler) in \cref{sec:cartesian-presentations}.
  In \cref{sec:symmoncat} we will do the somewhat trickier symmetric case; after which the reader should be able to handle the trickiest non-symmetric case in \cref{ex:moncat-pres}.
\end{rmk}


\subsection*{Exercises}

\begin{ex}\label{ex:repmulticat-moncat}
  Our proof of \cref{thm:moncat-initial} relied on the fact that monoidal categories are equivalent to representable multicategories, which we sketched but did not prove carefully.
  If we don't assume this fact, then our proof of \cref{thm:moncat-initial} is actually just about free representable multicategories.
  Using this version of the theorem, prove \emph{using type theory} that any representable multicategory is monoidal: that is, its tensor product is coherently associative and unital.
\end{ex}

\begin{ex}\label{ex:moncat-multisubadm}
  Formulate and prove the admissibility of a ``multi-substitution'' rule like \cref{thm:multiposet-multicutadm} for the type theories considered in this section.
\end{ex}

\begin{ex}\label{ex:moncat-context-splitting}
  The annotation $\Gamma|\Delta$ on $\match_{A\tensor B}^{\Gamma|\Delta}$ is something that appears only in the non-symmetric case, so we encourage the reader not to worry overmuch about it.
  However, for the reader who nevertheless insists on worrying, here is some extra reassurance.
  \begin{enumerate}
  \item We noted in \cref{thm:moncat-tad} that this annotation on $\match_{A\tensor B}^{\Gamma|\Delta}(M,xy.N)$ is only necessary if $M$ contains no variables.
    To see that it can actually matter in that case, find an example of two distinct derivations whose corresponding terms differ \emph{only} in their annotations $\Gamma|\Delta$.\label{item:moncat-context-splitting-1}
  % \begin{mathpar}
  %   \inferrule*{\ec\types \tpair\star\star:\one\tensor \one\\
  %     \inferrule*{
  %       x:\one \types x:\one\\
  %       \inferrule*{
  %         y:\one \types y:\one\\
  %         u:C \types u:C
  %       }{u:C,y:\one \types \match_\one(y,u):C}
  %     }{u:C,x:\one,y:\one \types \match_\one(x,\match_\one(y,u)):C}
  %   }{u:C \types \match_\tensor(\tpair\star\star, xy.\match_\one(x,\match_\one(y,u))) : C}
  %   \and
  %   \inferrule*{\ec\types \tpair\star\star:\one\tensor \one\\
  %     \inferrule*{
  %       x:\one \types x:\one\\
  %       \inferrule*{
  %         y:\one \types y:\one\\
  %         u:C \types u:C
  %       }{y:\one,u:C \types \match_\one(y,u):C}
  %     }{x:\one,y:\one,u:C \types \match_\one(x,\match_\one(y,u)):C}
  %   }{u:C \types \match_\tensor(\tpair\star\star, xy.\match_\one(x,\match_\one(y,u))) : C}
  % \end{mathpar}
  \item Prove that any two terms as in \ref{item:moncat-context-splitting-1} are related by $\equiv$.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:debruijn-context-concat}
  Describe precisely what has to happen to de-Bruijn-style variables when concatenating contexts, and formulate the rules for the type theories of this section using de Bruijn variables.
% Let us write $A[+n]$, $M[+n]$, $\Gamma[+n]$, and so on for the operation of adding $n$ to all the variable indices\footnote{Technically, all the \emph{free} variable indices; we will return to this in \cref{sec:moncat}.} in any syntactic object; thus for instance $f(x_1,x_2)[+3] = f(x_4,x_5)$.
% Also, if $\Gamma$ is a context, let us write $|\Gamma|$ for its length.
% Now if we use ``de Bruijn levels'', the concatenation of $\Gamma$ and $\Delta$ must be $\Gamma,\Delta[+|\Gamma|]$, while if we use ``de Bruijn indices'' it must be $\Gamma[+|\Delta|],\Delta$.
% For instance, we concatenate $x_1:A_1, x_2:A_2$ with $x_1:B_1$ to get $x_1:A_1, x_2:A_2,x_3:B_1$.
%
% \begin{rmk}
%   If we use de Bruijn style for variables, then this issue doesn't arise, but other confusing phenomena appear instead.
%   In general, when combining terms defined in different contexts using de Bruijn variables, we increment their variable numbers to match those in the new context.
%   For instance, given $x_1:A,x_2:B \types f(x_1,x_2):C$ and $x_1:D\types g(x_1):E$, we increment the latter when forming $x_1:A,x_2:B,x_3:D\types \tpair{f(x_1,x_2)}{g(x_3)}:C\tensor E$.
%   However, in a $\match_\tensor$ term, we can do this with the discriminee $M$ but not with the case branch $N$.
%   Inside $N$ in $\match_\tensor(M,x_i x_{i+1}.N)$, we need the variables $x_i$ and $x_{i+1}$ to refer to the ones being bound.
%   But if $\Psi$ contains fewer than two variables, then in the concatenated context $\Gamma,\Psi,\Delta$ some of the variables in $\Delta$ will also be named $x_i$ or $x_{i+1}$; so inside $N$ in $\match_\tensor(M,x_i x_{i+1}.N)$ we need to refer to variables in $\Delta$ by the numbers that they have in the original judgment $\Gamma,x_i:A,x_{i+1}:B,\Delta\types N:C$.
%   Thus, for instance, if $\Psi=()$ and $N$ is $x_1:A,x_2:B,x_3:D\types f(x_1,x_2,x_3):C$, then the result of $\tensorE$ must be $x_1:D \types \match(M,x_1 x_2.f(x_1,x_2,x_3)):C$, in which the variable denoted ``$x_3$'' in the term actually refers to the variable denoted ``$x_1$'' in the context.
%   (This example is for de Bruijn levels; de Bruijn indices, with the numbers going the other way, have a similar problem with $\Gamma$ in place of $\Delta$.)
%   There is no technical ambiguity and a computer can parse this term just fine, but it is fairly unreadable for a human.
%   (Indeed, according to Conor McBride, Bob Atkey once described the ability to read de Bruijn variables as a reverse Turing test.)
% \end{rmk}
\end{ex}


\section{Adding products and coproducts}
\label{sec:multicat-prod-coprod}

Now that we understand the simple type theories of multicategories and monoidal categories, let's add products and coproducts as well.
This is where we start to see the value of principle~\eqref{princ:independence} from \cref{sec:why-multicats}: for the most part we can just ``put together'' the rules from \cref{sec:multicat-moncat,sec:catprod,sec:catcoprod}, although there is a little extra work to generalize the rules for products and coproducts to the non-unary case.

In \cref{ex:monpos-mslat,ex:monpos-jslat} you studied sequent calculi for monoidal posets with meets and distributive monoidal posets.
Now we formulate similar rules in natural deduction style, annotated with terms; the entire \textbf{simple type theory for distributive monoidal categories with products} (except for the obvious rules governing the judgment $\types A\type$) is shown in \cref{fig:moncat-prod-coprod}.
(To obtain theories for monoidal categories with products only, or distributive monoidal categories, or multicategories with products and coproducts, and so on, we can simply omit some of these rules and their corresponding clauses in the following proofs.)

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{\types A\type}{x:A\types x:A}\;\idfunc
    \and
    \inferrule{f\in \cG(A_1,\dots,A_n;B) \\ \Gamma_1\types M_1:A_1 \\ \dots \\ \Gamma_n \types M_n:A_n}{\Gamma_1,\dots,\Gamma_n\types f(M_1,\dots,M_n):B}\;fI
    \and
    \inferrule{\Gamma\types M:A \\ \Delta\types N:B}{\Gamma,\Delta\types \tpair{M}{N}:A\tensor B}\;\tensorI
    \and
    \inferrule{
      \Psi \types M:A\tensor B \\
      \Gamma,x:A,y:B,\Delta\types N:C
    }{
      \Gamma,\Psi,\Delta \types \match_{A\tensor B}^{\Gamma|\Delta}(M,xy.N):C
    }\;\tensorE
    \\
    \inferrule{ }{\ec\types \ott:\one}\;\one I
    \and
    \inferrule{
      \Psi\types M:\one \\
      \Gamma,\Delta\types N:C
    }{
      \Gamma,\Psi,\Delta\types \match_\one(M,N):C
    }\;\one E
    \\
    \inferrule{\Gamma\types M:A \\ \Gamma\types N:B}{\Gamma\types \pair{M}{N} :A\times B}\;\timesI
    \and
    \inferrule{\Gamma\types M:A\times B}{\Gamma\types \pr1AB(M):A}\;\timesE1
    \and
    \inferrule{\Gamma\types M:A\times B}{\Gamma\types \pr2AB(M):B}\;\timesE2
    \\
    \inferrule{ }{x_1:A_1,\dots,x_n:A_n\types \ttt(x_1,\dots,x_n):\unit}\;\unit I
    \and
    \inferrule{\Psi\types M:\zero}{\Gamma,\Psi,\Delta\types \abort^{\Gamma,\Delta}(M):C}\;\zero E
    \\
    \inferrule{\Gamma\types M:A}{\Gamma\types \inl(M):A+B}\;\plusI1
    \and
    \inferrule{\Gamma\types N:B}{\Gamma\types \inr(N):A+B}\;\plusI2
    \and
    \inferrule{
      \Psi\types M:A+B \\ \Gamma,u:A,\Delta \types P:C \\ \Gamma,v:B,\Delta\types Q:C
    }{\Gamma,\Psi,\Delta \types\acase AB^{\Gamma|\Delta}(M,u.P,v.Q):C}\;\plusE
  \end{mathpar}
  \caption{Distributive monoidal categories with products}
  \label{fig:moncat-prod-coprod}
\end{figure}

A few things are worth remarking on.
Firstly, the types $\tensor,\one,+,\zero$ are ``positive'' (have ``mapping out'' universal properties), while the types $\times,\unit$ are ``negative'' (have ``mapping in'' universal properties).
All the positive types have elimination rules involving a $\match$ that binds variables (perhaps zero of them), while the negative types do not.
This is a general feature of the behavior of positive and negative types with respect to abstract variables.

Secondly, as in \cref{ex:monpos-jslat}, the elimination rules for $\zero$ and $A+B$ act on a single type in the context, leaving the others untouched.
This corresponds to the definition of coproducts in a multicategory from \cref{thm:multicat-coprod}.

Thirdly, notice the difference between $\one I$ and $\unit I$: both have no premises, but in $\one I$ the context of the conclusion must be empty, whereas in $\unit I$ it can be arbitrary.
Similarly, the difference between $\tensorI$ and $\timesI$ is that in $\tensorI$ the contexts are concatenated in the conclusion, while in $\timesI$ both premises must have the same context, which is repeated in the conclusion.

Finally, there are some curious annotations.
As in \cref{sec:moncat}, the superscripts $\Gamma|\Delta$ on $\match_\tensor$ and $\match_+$ are to ensure type-checking, and can usually be omitted; and similarly for the superscript $AB$ on $\pi_i$ as in \cref{sec:catprod}.
The superscript $\Gamma,\Delta$ on $\abort$, however, is there for a different purpose, which is the same purpose as the passing of all the variables in the context as arguments to $\ttt$; it has to do with linearity.

Unlike the theory of \cref{sec:multicat-moncat}, this type theory is not globally ``linear'': for instance in $x:A \types \pair x x : A\times A$ the variable $x$ appears twice.
But by including the unused variables in $\unit I$ and $\zero E$ we can ensure the following weaker property.

\begin{lem}\label{thm:moncat-prod-coprod-superlin}
  In any derivable sequent $\Gamma\types M:A$, every variable in $\Gamma$ appears at least once (free) in the term $M$.
\end{lem}
\begin{proof}
  An easy induction over derivations.
\end{proof}

This ``superlinearity'' property guarantees that terms are derivations.

\begin{lem}\label{thm:moncat-prod-coprod-tad}
  A derivable sequent $\Gamma\types M:A$ uniquely determines a derivation.
\end{lem}
\begin{proof}
  By induction as usual.
  The cases involving $f$, $\tensor$, and $\one$ are essentially just like in \cref{thm:moncat-tad}; \cref{thm:moncat-prod-coprod-superlin} ensures that each variable appears at least once in the term, and if the term is derivable then each variable must appear in only one subterm, determining the context splitting.
  The cases involving $\times,\unit,+,\zero$ are straightforward.
\end{proof}

A concrete example where we need the extra arguments to $\ttt$ is:
\begin{equation}\label{eq:ttt-arg}
  \inferrule*{\inferrule*{ }{x:A \types \ttt(x):\unit} \\
    \inferrule*{ }{\cdot \types \ttt():\unit}}
  {x:A \types \tpair{\ttt(x)}{\ttt()} : \unit\tensor\unit}
  \qquad
  \inferrule*{\inferrule*{ }{\ec\types \ttt():\unit} \\
    \inferrule*{ }{x:A \types \ttt(x):\unit}}
  {x:A \types \tpair{\ttt()}{\ttt(x)} : \unit\tensor\unit}
\end{equation}
Unlike with the annotations $\Gamma|\Delta$ on $\match$es (see \cref{ex:moncat-context-splitting}), these terms really can represent distinct morphisms (see \cref{ex:moncat-prod-coprod-context}).

\begin{thm}\label{thm:moncat-prod-coprod-subadm}
  Substitution is admissible in the {simple type theory for distributive monoidal categories with products}: given derivations of
  $\Gamma\types M:A$ and $\Delta,x:A,\Psi\types N:B$, we can construct a derivation of $\Delta,\Gamma,\Psi\types M[N/x]:B$.
  Moreover, it is associative and interchanging.
\end{thm}
\begin{proof}
  The defining equations are shown in \cref{fig:moncat-prod-coprod-sub}.
  They basically augment the rules from \cref{fig:moncat-sub} with versions of the rules from \cref{thm:catprod-subadm,thm:catcoprod-subadm}.
  Note the difference between the cases for $\tpair P Q$ and $\pair P Q$: in the first we recurse into only one of the subterms, while in the second we recurse into both.
  Also there are a couple of new rules for $\abort$ and $\case$ to deal with the fact that a free variable might occur in one of the case branches rather than the discriminee.
\end{proof}

\begin{figure}
  \centering
  \begin{alignat*}{2}
    x[M/x] &= M\\
    f(N_1,\dots,N_n)[M/x] &= f(N_1,\dots,N_i[M/x],\dots,N_n) &&\quad\text{if $x$ occurs in $N_i$}\\
    \tpair P Q[M/x] &= \tpair{P[M/x]}{Q} &&\quad\text{if $x$ occurs in $P$}\\
    \tpair P Q[M/x] &= \tpair{P}{Q[M/x]} &&\quad\text{if $x$ occurs in $Q$}\\
    \match_\tensor(N,uv.P)[M/x] &= \match_\tensor(N[M/x],uv.P) &&\quad\text{if $x$ occurs in $N$}\\
    \match_\tensor(N,uv.P)[M/x] &= \match_\tensor(N,uv.P[M/x]) &&\quad\text{if $x$ occurs in $P$}\\
    % \match_\tensor^{\Gamma|\Delta}(N,uv.P)[M/x] &= \match_\tensor^{\Gamma|\Delta}(N[M/x],uv.P) &&\quad\text{if $x$ occurs in $N$}\\
    % \match_\tensor^{\Gamma_1,x,\Gamma_2|\Delta}(N,uv.P)[M/x] &= \match_\tensor^{\Gamma_1,\Psi,\Gamma_2|\Delta}(N,uv.P[M/x]) &&\quad\text{$\Psi$ the context of $M$}\\
    % \match_\tensor^{\Gamma|\Delta_1,x,\Delta_2}(N,uv.P)[M/x] &= \match_\tensor^{\Gamma|\Delta_1,\Psi,\Delta_2}(N,uv.P[M/x]) &&\quad\text{$\Psi$ the context of $M$}\\
    \ott[M/x] &&&\quad\text{cannot happen}\\
    \match_\one(N,P)[M/x] &= \match_\one(N[M/x],P) &&\quad\text{if $x$ occurs in $N$}\\
    \match_\one(N,P)[M/x] &= \match_\one(N,P[M/x]) &&\quad\text{if $x$ occurs in $P$}\\
    \ttt(\vec y,x,\vec z)[M/x] &= \ttt(\vec y,\vec w, \vec z) &&\quad\text{$\vec w$ the free variables of $M$}\\
    (\pi_1(N))[M/x] &= \pi_1(N[M/x])\\
    (\pi_2(N))[M/x] &= \pi_2(N[M/x])\\
    \pair{P}{Q}[M/x] &= \pair{P[M/x]}{Q[M/x]}\\
    \abort(N)[M/x] &= \abort(N[M/x]) &&\quad\text{if $x$ occurs in $N$}\\
    \abort(N)[M/x] &= \abort(N) &&\quad\text{if $x$ not in $N$}\\
    \inl(N)[M/x] &= \inl(N[M/x])\\
    \inr(N)[M/x] &= \inr(N[M/x])\\
    \case(N,u.P,v.Q)[M/x] &= \case(N[M/x],u.P,v.Q) &&\quad\text{if $x$ occurs in $N$}\\
    \case(N,u.P,v.Q)[M/x] &= \case(N,u.P[M/x],v.Q[M/x]) &&\quad\text{if $x$ occurs in $P,Q$}
  \end{alignat*}
  \caption{Substitution for distributive monoidal categories with products}
  \label{fig:moncat-prod-coprod-sub}
\end{figure}

The $\beta$- and $\eta$-conversion rules are likewise obtained by combining those of \cref{sec:multicat-moncat,sec:catprod,sec:catcoprod}; they are shown in \cref{fig:moncat-prod-coprod-equiv}.

\begin{figure}
  \centering
  \begin{mathpar}
    \match_\tensor(\tpair M N,xy.P) \equiv P[M/x,N/y]\and
    \match_\tensor(M,xy.N[\tpair xy/u]) \equiv N[M/u]\\
    \match_\one(\ott,N) \equiv N\and
    \match_\one(M,N[\ott/u]) \equiv N[M/u]\\
    \pi_1(\pair M N) \equiv M\and
    \pi_2(\pair M N) \equiv N\\
    \pair{\pi_1(M)}{\pi_2(M)} \equiv M\and
    \ttt(x_1,\dots,x_n) \equiv M \\
    \case(\inl(M),u.P,v.Q) \equiv P[M/u]\and
    \case(\inr(M),u.P,v.Q) \equiv Q[M/v]\and
    \case(M,u.P[\inl(u)/y],v.P[\inr(v)/y]) \equiv P[M/y]\and
    \abort(M) \equiv P[M/y]\and
  \end{mathpar}
  \caption{Equality rules for distributive monoidal categories with products}
  \label{fig:moncat-prod-coprod-equiv}
\end{figure}

\begin{thm}\label{thm:moncat-prod-coprod-initial}
  The free distributive monoidal category with products generated by a multigraph \cG is presented by this theory in the usual way: its morphisms are the derivations of $\Gamma\types M$ (or the derivable terms $\Gamma\types M:A$) modulo $\equiv$.
\end{thm}
\begin{proof}
  As usual, \cref{thm:moncat-prod-coprod-subadm} gives us a multicategory, and the rules for the operations $\tensor,\one,\times,\ttt,+,\zero$ make it representable and give it products and coproducts.
  Initiality then follows by the usual induction over derivations.
\end{proof}

There are two important things to note here.
Firstly, while there are a lot of rules in this type theory, each of them is essentially something we already understood from a previous section, and we were able to put them together essentially independently without worrying about how they interact.
This is a good example of the ``modularity'' of type theory, and the value of principle~\eqref{princ:independence} from \cref{sec:why-multicats}.

Secondly, even though the rules for $\tensor$ and $+$ are completely independent, we nevertheless obtained a nontrivial interaction between them (distributivity), \emph{because of the structure of the context} and how it mirrors the categorical notion of multicategory.
This suggests that we could obtain further properties and relationships between type operations by modifying the judgmental/context structure.
The categorical side of this involves moving to \emph{generalized multicategories}.

\subsection*{Exercises}

\begin{ex}\label{ex:moncat-prod-coprod-context}
  Find an example of a distributive monoidal category with products in which the two terms in~\eqref{eq:ttt-arg} represent distinct morphisms.
\end{ex}


\section{Some generalized multicategories}
\label{sec:cartmulti}

% \subsection{Cartesian clubs}
% \label{sec:cart-clubs}

We want to consider monoidal categories with ``something extra'', such as symmetric monoidal categories or cartesian monoidal categories.
To describe a type theory for monoidal categories of this sort, principle~\eqref{princ:structural} from \cref{sec:why-multicats} suggests that we should ask what additional structure this ``something extra'' induces on their underlying multicategories.
Because the morphisms $(A_1,\dots,A_n) \to B$ in the underlying multicategory of a monoidal category \cC are, by definition, the morphisms $A_1\tensor\cdots\tensor A_n \to B$ in \cC, the answer to this question depends on what morphisms between tensor products exist ``generically'' in monoidal categories of our desired sort.
Here are some examples.
\begin{enumerate}
\item If \cC is a symmetric monoidal category, we have symmetry isomorphisms $A_1\tensor\cdots\tensor A_n\toiso A_{\sigma 1}\tensor\cdots\tensor A_{\sigma n}$ for any permutation $\sigma\in S_n$.
  Thus, by precomposing with these isomorphisms, we obtain functions between multicategorical hom-sets
  \begin{equation}
    \sigma^*: \cC(A_{\sigma 1},\dots,A_{\sigma n}; B) \to \cC(A_1,\dots,A_n;B)\label{eq:symm-multicat-action}
  \end{equation}
  that satisfy appropriate axioms.
\item If \cC is a cartesian monoidal category, we have symmetries but also diagonals such as $A\to A\times A$ and projections such as $A\times B \to B$.
  In general, for any function $\sigma : \{1,\dots,m\} \to \{1,\dots,n\}$ we have a morphism
  \[ A_1\times \cdots\times A_n \too A_{\sigma 1} \times\dots\times A_{\sigma m} \]
  whose component $A_1\times \cdots\times A_n \to A_{\sigma k}$ is the projection onto the $(\sigma k)^{\mathrm{th}}$ factor.
  Precomposition with these morphisms yields analogous functions
  \begin{equation}
    \sigma^*: \cC(A_{\sigma 1},\dots,A_{\sigma m}; B) \to \cC(A_1,\dots,A_n;B).\label{eq:cartmulticat-action}
  \end{equation}
\item Less well-known than symmetric and cartesian monoidal categories are \emph{semicartesian} monoidal categories, whose unit object is the terminal object, but whose tensor product is not necessarily the cartesian product.
  (An example familiar to higher category theorists is the category $\mathbf{2Cat}$ with its Gray tensor product.)
  We will always assume that semicartesian monoidal categories are additionally symmetric.
  The semicartesianness gives us projections but not diagonals, leading to functions~\eqref{eq:cartmulticat-action} whenever $\sigma$ is \emph{injective}.
\item Even less well-known are \emph{relevance} monoidal categories, which are symmetric and equipped with a coherent system of diagonals $A \to A\tensor A$ but whose unit object is not in general terminal.
  A familiar example is the category of pointed sets with its smash product~\cite{dp:relevant-cats}.
  In this case we have functions~\eqref{eq:cartmulticat-action} only when $\sigma$ is \emph{surjective}.
\end{enumerate}

All of these cases can be encompassed by the following definitions.

\begin{defn}
  Let \fN be the full subcategory of \bSet whose objects are the sets $\{1,\dots, n\}$ for all integers $n\ge 0$.
  We regard it as a \emph{cocartesian} strict monoidal category, under the disjoint union operation $\{1,\dots,n\} \sqcup \{1,\dots,m\} = \{1,\dots,n+m\}$.
  Moreover, for any $\sigma : \{1,\dots,m\} \to \{1,\dots,n\}$ and $k_1,\dots,k_n$, let $\sigma \wr (k_1,\dots,k_n)$ denote the composite function
  \begin{equation*}
    \{1,\dots,\textstyle\sum_{i=1}^m k_{\sigma i} \}
     \toiso \bigsqcup_{i=1}^m \{1,\dots,k_{\sigma i}\}
     \xto{\widehat{\sigma}} \bigsqcup_{j=1}^n \{1,\dots,k_{j}\}
     \toiso \{1,\dots,\textstyle\sum_{j=1}^n k_j \}
  \end{equation*}
  where $\widehat{\sigma}$ acts as the identity from the $i^{\mathrm{th}}$ summand to the $(\sigma i)^{\mathrm{th}}$ summand.
  A \textbf{faithful cartesian club} is a subcategory $\fS\subseteq \fN$ such that
  \begin{enumerate}
  \item \fS contains all the objects of \fN.
  \item \fS is closed under the cocartesian monoidal structure, i.e.\ if $\sigma$ and $\tau$ are morphisms of $\fS$ then so is $\sigma\sqcup \tau$.
  \item \fS is closed under $\wr$, i.e.\ whenever it contains $\sigma$ it also contains $\sigma \wr (k_1,\dots,k_n)$.
  \end{enumerate}
\end{defn}

The above examples are the cases when \fS consists of the bijections, all the functions, the injections, or the surjections respectively.
There is also the trivial case when \fS contains only the identities.

\begin{defn}\label{defn:fS-multicategory}
  Let \fS be a faithful cartesian club.
  An \textbf{\fS-multicategory} is a multicategory \cM together with operations
  \begin{align*}
    \cM(A_{\sigma 1},\dots,A_{\sigma m}; B) &\to \cM(A_1,\dots,A_n;B)\\
    f &\mapsto f\sigma^*
  \end{align*}
  for all functions $\sigma : \{1,\dots,m\} \to \{1,\dots,n\}$ in \fS, satisfying the following axioms:
  \begin{enumerate}
  \item $f \sigma^* \tau^* = f(\tau\sigma)^*$\label{item:cartmulti-1}
  \item $f (\idfunc_n)^* = f$\label{item:cartmulti-2}
  \item $g\circ (f_1 \sigma_1^* ,\dots, f_n \sigma_n^*) = (g \circ (f_1,\dots,f_n))(\sigma_1\sqcup \cdots \sqcup \sigma_n)^*$\label{item:cartmulti-3}
  \item $g\sigma^* \circ (f_1,\dots,f_n) = (g\circ (f_{\sigma 1},\dots, f_{\sigma m}))(\sigma \wr (k_1,\dots,k_n))^*$ where $k_i$ is the arity of $f_i$.\label{item:cartmulti-4}
  \end{enumerate}
  If each hom-set $\cM(A_1,\dots,A_n;B)$ has at most one element, we call \cM an \textbf{\fS-multiposet}.
  An \textbf{\fS-multigraph} is a multigraph equipped with similar operations satisfying~\ref{item:cartmulti-1} and~\ref{item:cartmulti-2}.
\end{defn}

As special cases we have, by definition:
\begin{center}
\begin{tabular}{c|c}
  When $\fS=$ & $\fS$-multicategories are called\\\hline
  bijections & \textbf{symmetric multicategories}\\
  all functions & \textbf{cartesian multicategories}\\
  injections & \textbf{semicartesian (symmetric) multicategories}\\
  surjections & \textbf{relevance multicategories}\\
  only identities & (ordinary) multicategories
\end{tabular}
\end{center}

% \subsection{Products in \fS-multicategories}
% \label{sec:cartmulti-prod}

Now, recall the definition of tensor products in a multicategory from \cref{defn:multicat-tensor}, and the result of \cref{thm:multicat-repr} that having all tensor products (being ``representable'') is equivalent to being a monoidal category.
For a general faithful cartesian club \fS, we might as well \emph{define} an \textbf{\fS-monoidal category} to be an \fS-multicategory that is representable.
However, in many cases this is equivalent to a more familiar notion.

\begin{thm}\label{thm:symm-multicat-repr}
  If \fS includes all bijections, then the monoidal category obtained from any representable \fS-multicategory is symmetric.
  Moreover, the equivalence of \cref{thm:multicat-repr} induces an equivalence between representable symmetric multicategories and symmetric monoidal categories.
\end{thm}
\begin{proof}
  If $\chi : (A,B) \to A\tensor B$ is a tensor product, then by acting on it with the transposition $\sigma : \{1,2\} \toiso \{1,2\}$ we obtain a morphism $\chi\sigma^* : (B,A) \to A\tensor B$.
  Applying the universal property of the tensor product $(B,A) \to B\tensor A$, we get a map $B\tensor A \to A\tensor B$.
  We can similarly use the universal property to check the symmetry axioms.

  Conversely, the coherence theorem for symmetric monoidal categories yields isomorphisms~\eqref{eq:symm-multicat-action}, composing with which gives its underlying multicategory a symmetric structure.
  It is straightforward to verify that these constructions are inverses up to isomorphism.
\end{proof}

Recall from \cref{sec:multicats-catth} the definition of products in a multicategory.

\begin{thm}\label{thm:semicart-multicat-repr}
  If \fS includes all injections, then an object $\one$ is terminal if and only if it is a unit object (i.e.\ there is a universal tensor product morphism $()\to \one$).
  Moreover, the equivalence of \cref{thm:multicat-repr} induces an equivalence between representable semicartesian multicategories and semicartesian monoidal categories.
\end{thm}
\begin{proof}
  If \fS includes injections, then for any $A_1,\dots,A_n$ the injection $\emptyset \to \{1,\dots,n\}$ induces a map
  \[ \cM(;B) \to \cM(A_1,\dots,A_n;B). \]
  Thus, if $\one$ is a unit object with universal morphism $\chi:()\to \one$, then this gives us induced maps $e_{A_1,\dots,A_n}:(A_1,\dots,A_n) \to \one$.
  Moreover, the fourth ``equivariance'' axiom of an \fS-multicategory implies that these maps are natural, in the sense that
  $e_{A_1,\dots,A_n} \circ (f_1,\dots,f_n) = e_{B_1,\dots,B_m}$ for any $f_1,\dots,f_n$.
  In particular, $e_{\one} \circ \chi = e_{()} = \chi$; so by the universal property of $\chi$, we have $e_{\one} = \idfunc_{\one}$.
  A standard argument (generalized from categories to multicategories) now implies that $\one$ is terminal.

  Conversely, suppose $\unit$ is terminal.
  Then in particular, we have a unique morphism $\chi : ()\to \unit$, and acting on $\chi$ by the injection $\emptyset \to \{1,\dots,n\}$ can only yield the unique morphism $(A_1,\dots,A_n)\to \unit$.
  Now we have to show that
  \[ (-\circ_{n+1} \chi) : \cM(A_1,\dots,A_n,\unit,B_1,\dots,B_m; C) \to \cM(A_1,\dots,A_n,B_1,\dots,B_m; C) \]
  is a bijection.
  But we have a map in the other direction given by acting with an appropriate injection, and the equivariance properties imply that this is an inverse.

  Lastly, if we have a semicartesian monoidal category, then for any injection $\sigma$ we have a map
  \[ A_1\tensor \cdots\tensor A_n \too A_{\sigma 1} \tensor\dots\tensor A_{\sigma m} \]
  defined by mapping each $A_j$ not in the image of $\sigma$ to the terminal object $1$, then removing those copies of $1$ from the tensor product since they are also the tensor unit (and finally permuting if necessary).
  It is straightforward to verify that these actions give a semicartesian multicategory, and that that these constructions are inverses up to isomorphism.
\end{proof}

\begin{thm}\label{thm:cart-multicat-repr}
  If \fS consists of all functions (i.e.\ we are in a cartesian multicategory), then products $A\times B$ are in bijective correspondence with tensor products $A\tensor B$.
  Moreover, the equivalence of \cref{thm:multicat-repr} induces an equivalence between representable cartesian multicategories and cartesian monoidal categories (i.e.\ categories with finite products).
\end{thm}
\begin{proof}
  By acting with injections, for any $A,B$ we obtain morphisms $(A,B)\to A$ and $(A,B)\to B$.
  Thus, if $A\times B$ is a product, we have an induced map $\chi:(A,B)\to A\times B$.
  Now if we have any morphism $(C_1,\dots,C_n,A,B,D_1,\dots,D_m)\to E$, we can compose with the two projections of the product to get a morphism $(C_1,\dots,C_n,A\times B,A\times B,D_1,\dots,D_m)\to E$, and then act by a surjection to get $(C_1,\dots,C_n,A\times B,D_1,\dots,D_m)\to E$.
  The equivariance properties of a cartesian multicategory, and the universal property of the product, imply that this operation is inverse to composing with $\chi$, so that the latter is a tensor product.

  Conversely, if $\chi:(A,B)\to A\tensor B$ is a tensor product, by applying its universal property to the above morphisms $(A,B)\to A$ and $(A,B)\to B$ we obtain projections $A\tensor B \to A$ and $A\tensor B\to B$.
  Now given $f:(C_1,\dots,C_n)\to A$ and $g:(C_1,\dots,C_n)\to B$, we have $\chi\circ (f,g) : (C_1,\dots,C_n,C_1,\dots,C_n) \to A\tensor B$, and by acting with a suitable surjection we get $(C_1,\dots,C_n)\to A\tensor B$.
  Again, the equivariance properties and the universal property of the tensor product imply that this is a unique factorization of $f$ and $g$ through the projections.
\end{proof}

Note although the first conclusion of \cref{thm:cart-multicat-repr} refers only to binary products, it still requires the presence of \emph{injections} in \fS in addition to surjections.
Indeed, the monoidal category of pointed sets with its smash product has an underlying multicategory that is relevance (i.e.\ admits an action by all surjections), but the smash product is different from the cartesian product.
It is also possible to characterize the \fS-monoidal categories when \fS is the injections, but we leave this to the interested reader; see \cref{ex:relevance-moncat}.

\begin{rmk}\label{rmk:absolute}
  \cref{thm:semicart-multicat-repr,thm:cart-multicat-repr} identify an object having a ``mapping out'' universal property (a tensor product or unit object in a multicategory) with an object having a ``mapping in'' universal property (a cartesian product or terminal object), in the strong sense that if either exists then it is also the other.
  This sort of ``ambidextrous'' universal property appears elsewhere in category theory as well.
  For instance, the splitting of an idempotent can be regarded as either a limit or a colimit; in a category enriched over abelian monoids, finite products and coproducts coincide; and more generally for any kind of enrichment there is a notion of ``absolute (co)limit''~\cite{street:absolute}.
  Thus, although multicategories are not ``enriched categories'' in the usual sense, we could say informally that in a cartesian multicategory products are absolute limits, while in a semicartesian multicategory terminal objects are.
  See also \cref{ex:absolute}.
\end{rmk}

Finally, we observe that closedness can be naturally characterized multicategorically.
Suppose for simplicity that \fS contains at least all bijections.
Then we say an \fS-multicategory is \textbf{closed} if for each pair of objects $A$ and $B$ there is a specified object $A\hom B$ and a morphism $\chi : (A\hom B,A) \to B$ postcomposition with which defines bijections
\[ (\chi\circ_1 -): \cM(C_1,\dots,C_n;A\hom B) \toiso \cM(C_1,\dots,C_n,A;B) \]
for all $C_1,\dots,C_n$.
(If \fS does not contain the bijections, we would just have to consider ``left and right closedness'' separately.)
The following is then straightforward.

\begin{thm}\label{thm:moncat-repr-closed}
  A symmetric monoidal category is closed if and only if its underlying multicategory is.
  Moreover, for all the above values of \fS that contain the bijections, this defines an equivalence of categories.\qed
\end{thm}

Of course, cartesian closed categories are just closed cartesian monoidal categories, so they are equivalent to closed cartesian multicategories.

\subsection*{Exercises}

\begin{ex}\label{ex:gen-multicat-repr}
  Fill in the details in the proof of \cref{thm:symm-multicat-repr,thm:semicart-multicat-repr,thm:cart-multicat-repr}.
\end{ex}

\begin{ex}\label{ex:club-generators}
  Let \fS be a faithful cartesian club.
  \begin{enumerate}
  \item Prove that if \fS contains the transposition $\{1,2\}\toiso \{1,2\}$, then it contains all bijections.
  \item Prove that if \fS contains the transposition $\{1,2\}\toiso \{1,2\}$ and also the injection $\emptyset \to \{1\}$, then it contains all injections.
  \item Prove that if \fS contains the transposition $\{1,2\}\toiso \{1,2\}$ and also the surjection $\{1,2\} \to \{1\}$, then it contains all surjections.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:cartmulti-oneplace}
  Define one-place versions of \fS-multicategories and show that they are equivalent to the multi-composition version defined in the text.
\end{ex}

\begin{ex}\label{ex:distrib}
  Show that representable cartesian multicategories with coproducts are equivalent to distributive categories.
\end{ex}

\begin{ex}\label{ex:absolute}
  Of course, for any \fS a \textbf{functor} between \fS-multicategories is required to preserve the $\sigma$-actions.
  Prove that:
  \begin{enumerate}
  \item Any functor between semicartesian multicategories must preserve unit objects / terminal objects.
  \item Any functor between cartesian multicategories must preserve tensor products / cartesian products.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:relevance-moncat}
  Define a notion of \textbf{relevance monoidal category}, by adding ``natural diagonals'' to a symmetric monoidal category, and show that such monoidal categories are equivalent to representable relevance multicategories.
  (See~\cite{dp:relevant-cats}.)
\end{ex}

\begin{ex}\label{ex:cocartesian-clubs}
  Define a notion of \textbf{faithful cocartesian club} and a corresponding notion of generalized multicategory that includes \emph{cocartesian} monoidal categories as the maximal case.
\end{ex}


\section{Intuitionistic logic}
\label{sec:logic}

We are now aiming at type theories for the generalized multicategories considered in \cref{sec:cartmulti}, along with the extra structures that they may have (tensor products, cartesian products, coproducts, and closedness).
In this section we start with the posetal case, which is also where our type theory at last begins to look rather like \emph{logic}.

\subsection{\fS-monoidal lattices}
\label{sec:monoidal-lattices}

According to principle~\eqref{princ:structural} from \cref{sec:why-multicats}, the additional action by $\sigma$'s in an \fS-multicategory should be represented by \emph{structural rules} in a type theory.
These rules are generally formulated and named as follows.
\begin{mathpar}
  \inferrule*[right=exchange]{\Gamma,A,B,\Delta\types C}{\Gamma,B,A,\Delta\types C}\and
  \inferrule*[right=weakening]{\Gamma,\Delta\types C}{\Gamma,A,\Delta\types C}\and
  \inferrule*[right=contraction]{\Gamma,A,A,\Delta\types C}{\Gamma,A,\Delta\types C}\and
\end{mathpar}
The correspondence between kinds of multicategory and structural rules\footnote{One can consider weakening and/or contraction without exchange, just as one might consider non-symmetric semicartesian or relevance multicategories.
  But this takes us rather far afield from categorical structures of general interest, so we leave it to the reader.} should not be surprising:
\begin{center}
\begin{tabular}{c|c}
  $\fS$-multicategories & structural rules\\\hline
  {symmetric multicategories} & exchange\\
  {cartesian multicategories} & exchange, weakening, contraction\\
  {semicartesian (symmetric) multicategories} & exchange, weakening\\
  {relevance multicategories} & exchange, contraction
\end{tabular}
\end{center}
Note that these structural rules refer only to single transpositions, projections, and duplications, rather than arbitrary functions in \fS.
This is similar to how, as we have noted, cut is usually stated in type theory using one-place composites rather than a multi-composition.
As in that case, the smaller operations suffice to generate the more general ones (c.f.\ \cref{ex:club-generators}).

What is somewhat less clear is how these rules can be made \emph{admissible} in line with principle~\eqref{princ:adm}.
For now let us ignore this question and take these rules (when we want them) as \emph{primitive} (recall \cref{rmk:admissible-derivable-1}).
This makes the treatment more parametric in \fS, and makes little difference for presenting free posets, since in that case we are only interested in the existence or nonexistence of derivations.
We will address the question of admissibility in \cref{sec:heyting-algebras,sec:stlc,sec:symmoncat}.

For the rest of this subsection, let \fS be one of the four possibilities above (so in particular, it will always contain the bijections).
All our type theories will then include the appropriate primitive structural rules, according to the above table.
Our type operations will be the posetal versions of all the ones we saw in \cref{sec:multicat-prod-coprod} --- $\tensor,\one,\meet,\top,\join,\bot$ --- and also an internal-hom for $\tensor$, which we denote by $A\hom B$.
(We postponed introducing the internal-hom until now only to avoid worrying about left- versus right-closedness in non-symmetric multicategories.)
Thus, the categorical structure in question is \emph{closed \fS-monoidal lattices}.
Of course, as in \cref{sec:multicat-prod-coprod} we can remove any of these operations without affecting the others, obtaining a type theory for weaker categorical structures.

The primitive rules of the \textbf{natural deduction for closed \fS-monoidal lattices} are shown in \cref{fig:natded-logic}.
Except for the structural rules (discussed above) and $\hom$, they are all obtained by removing the term annotations from the theory of \cref{sec:multicat-prod-coprod}.
The only other change is that since we always include the exchange rule as primitive, in the rules $\tensorE,\one E,\joinE,\zero E$ we don't need to put $\Psi$ in the middle of the context but are free to put it on one side.
As usual, we have also omitted the rules for the judgment $\types A\type$, which just say that all the objects of $\cG$ are types, as are $\one,\top,\bot$ and $A\tensor B, A\meet B, A\join B, A\hom B$ if $A$ and $B$ are.

\begin{figure}
  \centering
  \begin{mathpar}
  \inferrule*[right=exchange]{\Gamma,A,B,\Delta\types C}{\Gamma,B,A,\Delta\types C}\\
  \inferrule*[right=weakening]{\Gamma,\Delta\types C}{\Gamma,A,\Delta\types C}\;\text{if injections}\subseteq\fS\\
  \inferrule*[right=contraction]{\Gamma,A,A,\Delta\types C}{\Gamma,A,\Delta\types C}\;\text{if surjections}\subseteq\fS\\
  \inferrule{\types A\type}{A\types A}\and
  \inferrule{(A_1,\dots,A_n \le B)\in\cG \\ \Gamma_1\types A_1 \\ \dots \\ \Gamma_n \types A_n}{\Gamma_1,\dots,\Gamma_n\types B}\and
  \inferrule{\Gamma\types A \\ \Delta\types B}{\Gamma,\Delta\types A\tensor B}\;\tensorI\and
  \inferrule{
    \Psi \types A\tensor B \\
    \Gamma,A,B\types C
  }{
    \Gamma,\Psi \types C
  }\;\tensorE\\
  \inferrule{ }{\ec\types \one}\;\one I\and
  \inferrule{
    \Psi\types \one \\
    \Gamma\types A
  }{
    \Gamma,\Psi\types C
  }\;\one E\\
    \inferrule{\Gamma\types A \\ \Gamma\types B}{\Gamma\types A\meet B}\;\meetI
    \and
    \inferrule{\Gamma\types A\meet B}{\Gamma\types A}\;\meetE1
    \and
    \inferrule{\Gamma\types A\meet B}{\Gamma\types B}\;\meetE2
    \\
    \inferrule{ }{\Gamma\types \top}\;\top I
    \and
    \inferrule{\Psi\types \bot}{\Gamma,\Psi\types C}\;\bot E
    \\
    \inferrule{\Gamma\types A}{\Gamma\types A\join B}\;\joinI1
    \and
    \inferrule{\Gamma\types B}{\Gamma\types A\join B}\;\joinI2
    \and
    \inferrule{
      \Psi\types A\join B \\ \Gamma,A \types C \\ \Gamma,B\types C
    }{\Gamma,\Psi \types C}\;\joinE\\
    \inferrule{\Gamma,A\types B}{\Gamma\types A\hom B}\;\homI\and
    \inferrule{\Psi\types A\\\Gamma\types A\hom B}{\Gamma,\Psi\types B}\;\homE
  \end{mathpar}
  \caption{Natural deduction for closed \fS-monoidal lattices}
  \label{fig:natded-logic}
\end{figure}

The introduction rule for $\hom$ is simply one direction of its universal property from \cref{sec:multicats-catth}.
The elimination rule is the inverse direction, but with a cut built in to make the context of the conclusion general (modulo a splitting).
That is, $\homE$ can be derived from the opposite of $\homI$ and cut:
\begin{mathpar}
  \inferrule*{\Psi\types A\\ \inferrule*{\Gamma\types A\hom B}{\Gamma,A\types B}}{\Gamma,\Psi\types B}
\end{mathpar}
Note that, as promised in \cref{sec:why-multicats}, by using sequents with multiple types in the context, we can formulate the rules for $\hom$ without reference to $\meet/\times$.

The contraction rule gives the cut-admissibility theorem a new wrinkle.
Let us first consider the cases without contraction, which are more straightforward.

\begin{lem}\label{thm:natded-logic-cutadm}
  If \fS consists of the bijections or the injections, then cut is admissible in the natural deduction for closed \fS-monoidal lattices: if we have derivations of $\Psi\types A$ and $\Gamma,A,\Delta\types B$ then we also have $\Gamma,\Psi,\Delta\types B$.
\end{lem}
\begin{proof}
  As always, we induct on the derivation of $\Gamma,A,\Delta\types B$.
  The cases for most of the connectives are just like those in \cref{thm:moncat-prod-coprod-subadm}, and those for $\hom$ are nothing new.
  However, now we have a new possibility: the derivation might end with a primitive structural rule (exchange or weakening --- our hypothesis on \fS rules out contraction).

  Firstly, if the structural rule does not affect the type $A$, then we can simply commute it past the cut.
  For instance, if we have $\Psi\types A$ and $\Gamma,A,\Delta_1,C,\Delta_2\types B$ arising by weakening from $\Gamma,A,\Delta_1,\Delta_2\types B$, we can inductively obtain $\Gamma,\Psi,\Delta_1,\Delta_2\types B$ and then apply weakening again to get $\Gamma,\Psi,\Delta_1,C,\Delta_2\types B$.

  Secondly, essentially the same is true if it is an exchange that does affect $A$.
  For instance, if we have $\Psi\types A$ and $\Gamma,A,C,\Delta\types B$ arising by exchange from $\Gamma,C,A,\Delta\types B$, we can inductively obtain $\Gamma,C,\Psi,\Delta\types B$, and then re-apply exchange once for each type in $\Psi$ to get $\Gamma,\Psi,C,\Delta\types B$.
  (It does matter here that we have formulated the admissible cut rule {with} $A$ in the middle of the context rather than on one side, even though we have the exchange rule; otherwise the induction would fail to go through here.)

  Finally, suppose it is a weakening that affects $A$, so we have $\Psi\types A$ and $\Gamma,A,\Delta\types B$ arising by weakening from $\Gamma,\Delta\types B$.
  In this case we can forget about the derivation of $\Psi\types A$ and just weaken $\Gamma,\Delta\types B$ once for each type in $\Psi$ to get $\Gamma,\Psi,\Delta\types B$.
\end{proof}

If we try to extend this to theories with contraction, however, we have a problem.
Suppose the derivation of $\Gamma,A,\Delta\types B$ ends with a contraction that affects $A$, so that we have $\Psi\types A$ and $\Gamma,A,\Delta\types B$ arising by contraction from $\Gamma,A,A,\Delta\types B$.
Then we would like to inductively cut the latter with $\Psi\types A$ twice to obtain $\Gamma,\Psi,\Psi,\Delta\types B$, transforming
\begin{equation*}
  \inferrule*[right=cut]{\Psi\types A \\
  \inferrule*[Right=contraction]{\Gamma,A,A,\Delta\types B}{\Gamma,A,\Delta\types B}}{\Gamma,\Psi,\Delta\types B}
\end{equation*}
into
\begin{equation*}
  \inferrule*[Right=cut]{\Psi\types A\\
    \inferrule*[Right=cut]{\Psi\types A\\\Gamma,A,A,\Delta\types B}{\Gamma,\Psi,A,\Delta,\types B}}
  {\Gamma,\Psi,\Psi,\Delta\types B}
\end{equation*}
After this we could apply exchanges to pair up the two copies of each type in $\Psi$, and finally a contraction on each of them to eliminate the duplicates.
However, now we have the sort of problem that we did in the proof of \cref{thm:monpos-cutadm}: the derivation of $\Gamma,\Psi,A,\Delta,\types B$ that we obtain from our first application of the inductive hypothesis may not be ``smaller'' than our given derivation, so we cannot apply the inductive hypothesis to it again.
Moreover, the solution sketched there (inducting first on types and then on derivations) does not work here, since the types are not changing.

The standard solution used in type theory is to generalize the cut rule to a rule called ``mix'' that enables the induction to go through.
In our case, the mix rule says that if we have derivations of $\Psi\types A$ and $\Gamma\types B$, where $\Gamma$ contains one or more copies of $A$, then we can construct a derivation of $\Psi,\Gamma^A\types B$, where $\Gamma^A$ is $\Gamma$ with one or more copies of $A$ removed.
In other words, we build a certain amount of contraction into the induction hypothesis.
This works, but a more categorically principled solution is to use the multi-cut as in \cref{thm:monpos-multicutadm}.
This amounts to approximately the same thing, but feels less \textit{ad hoc} to a category theorist (at least, it does to the author).

\begin{lem}\label{thm:natded-logic-multicutadm}
  For any of our four \fS's, multi-cut is admissible in the natural deduction for closed \fS-monoidal lattices: if we have derivations of $\Psi_i\types A_i$ for $1\le i\le n$, and also $A_1,\dots,A_n \types B$, then we can construct a derivation of $\Psi_1,\dots,\Psi_n\types B$.
\end{lem}
\begin{proof}
  The non-structural rules are easy, just as before.
  (Recall that in general, cut is very straightforward for natural deductions because all the rules act only on the right.
  With this in mind it is unsurprising that primitive structural rules are problematic, since they act on the left.)

  Now, however, the structural rules are almost just as easy.
  If our derivation of $A_1,\dots,A_n \types B$ ends with an exchange, we can simply switch two of the derivations $\Psi_i\types A_i$ and induct.
  Similarly, if it ends with a weakening, we can just forget about one of the $\Psi_i\types A_i$ and induct.
  Finally, if it ends with a contraction, we can again induct on the premise, using one of the derivations $\Psi_i\types A_i$ twice.
\end{proof}

Now we can prove the initiality theorem just as usual.

\begin{thm}\label{thm:natded-logic-initial}
  For any relational multigraph \cG and any of our four \fS's, the free closed \fS-monoidal lattice on \cG can be presented by this natural deduction, with $(A_1,\dots,A_n)\le B$ holding just when $A_1,\dots,A_n\types B$ is derivable.
\end{thm}
\begin{proof}
  \cref{thm:natded-logic-multicutadm} (together with the identity rule) gives us a multiposet, the rules for the type operations make it representable, closed, and a lattice, and the structural rules make it an \fS-multiposet.
  Thus it lives in the correct category; and its freeness follows by induction as usual.
\end{proof}

We can also generalize from relational multigraphs to an appropriate kind of ``presentation'' as in \cref{sec:unary-theories}.
Since we are in the posetal case, things are much simpler because everything coincides with its 1-skeleton.
% and there is no need to worry about fancy kinds of naturality as in \cref{sec:tensor-presentations}.
Specifically, a \textbf{relational $(\tensor,\meet,\join,\hom)$-presentation} consists of
\begin{enumerate}
\item A set $\cP_0$ of objects; and
\item A relation $\cP_1$ between finite lists of types and single types, where the types are generated from $\cP_0$ by the rules for the judgment $\types A\type$ in the type theory for closed (\fS-)monoidal lattices.
\end{enumerate}
We can then construct a two-level tower of adjunctions generating a closed \fS-monoidal lattice from any such presentation.
The only other thing to be said about this is that in the posetal case, it is common to refer to the relations in $\cP_1$ as the \textbf{axioms}, since they are mere properties, in contrast to how in \cref{sec:theories} we used that word for the generating equalities (at level 2 rather than level 1).


\subsection{Heyting algebras}
\label{sec:heyting-algebras}

Let us now specialize to the cartesian case, where we have all three structural rules.
Thus the categorical structure in question is \emph{cartesian closed lattices}, which are also known as \textbf{Heyting algebras}.
This theory is simpler because $\tensor$ and $\one$ coincide with $\meet$ and $\top$ (see \cref{ex:cart-typetheory}), so we can omit the former ones.
A second reason it is simpler is because it is easy to make the structural rules admissible.
The key observation is the following.

\begin{lem}\label{thm:cart-constctx}
  In the presence of exchange, contraction, and weakening, the following rules are inter-derivable with the rules $\bot E$, $\joinE$, $\homE$ from \cref{fig:natded-logic}.
  \begin{mathpar}
    \inferrule{\types A\type \\ A\in \Gamma}{\Gamma\types A}\;\idfunc'
    \and
    \inferrule{(A_1,\dots,A_n \le B)\in\cG \\ \Gamma\types A_1 \\ \dots \\ \Gamma \types A_n}{\Gamma\types B}\;f'
    \and
    \inferrule{\Gamma\types \bot}{\Gamma\types C}\;\bot E'
    \and
    \inferrule{
      \Gamma\types A\join B \\ \Gamma,A \types C \\ \Gamma,B\types C
    }{\Gamma \types C}\;\joinE'
    \and
    \inferrule{\Gamma\types A\hom B \\ \Gamma\types A}{\Gamma\types B}\;\homE'
  \end{mathpar}
\end{lem}
\begin{proof}
  Here are the referenced rules from \cref{fig:natded-logic}:
  \begin{mathpar}
    \inferrule{\types A\type}{A\types A}\;\idfunc
    \and
    \inferrule{(A_1,\dots,A_n \le B)\in\cG \\ \Gamma_1\types A_1 \\ \dots \\ \Gamma_n \types A_n}{\Gamma_1,\dots,\Gamma_n\types B}\;f
    \and
    \inferrule{\Psi\types \bot}{\Gamma,\Psi\types C}\;\bot E
    \and
    \inferrule{
      \Psi\types A\join B \\ \Gamma,A \types C \\ \Gamma,B\types C
    }{\Gamma,\Psi \types C}\;\joinE
    \and
    \inferrule{\Gamma\types A\hom B \\ \Psi\types A}{\Gamma,\Psi\types B}\;\homE
  \end{mathpar}
  Clearly $\idfunc$ is a special case of $\idfunc'$, while conversely $\idfunc'$ can be derived from $\idfunc$ followed by weakening.
  And $\bot E'$ is a special case of $\bot E$, while $f'$ and $\joinE'$ and $\homE'$ can be derived from $f$ and $\joinE$ and $\homE$ followed by exchange and contraction to turn contexts like $\Gamma,\Gamma$ into $\Gamma$.
  Conversely, given the premises of any of these ``unprimed'' rules, we can weaken each $\Gamma$ and $\Psi$ to $\Gamma,\Psi$ (or $\Gamma_i$ to $\Gamma_1,\dots,\Gamma_n$ in the case of $f$), then apply the primed version of that rule to deduce the conclusion of the unprimed rule.
\end{proof}

If we replace the rules in question by their modified versions, then all the rules will have the property that the context of the conclusion is arbitrary, while the context of the premises differ from the context of the conclusion at most by addition of a new type.
In other words, as we proceed \emph{down} a derivation tree, we only ever \emph{remove} types from the context; and dually as we proceed \emph{up} a tree we only ever \emph{add} to the context.
This will enable us to ``push the structural rules up'' past all primitive rules until we get to $\idfunc$, thereby making them admissible.

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{\types A\type \\ A\in \Gamma}{\Gamma\types A}\;\idfunc
    \and
    \inferrule{(A_1,\dots,A_n \le B)\in\cG \\ \Gamma\types A_1 \\ \dots \\ \Gamma \types A_n}{\Gamma\types B}\;f
    \and
    \inferrule{\Gamma\types A \\ \Gamma\types B}{\Gamma\types A\meet B}\;\meetI
    \and
    \inferrule{\Gamma\types A\meet B}{\Gamma\types A}\;\meetE1
    \and
    \inferrule{\Gamma\types A\meet B}{\Gamma\types B}\;\meetE2
    \\
    \inferrule{ }{\Gamma\types \top}\;\top I
    \and
    \inferrule{\Gamma\types \bot}{\Gamma\types C}\;\bot E
    \\
    \inferrule{\Gamma\types A}{\Gamma\types A\join B}\;\joinI1
    \and
    \inferrule{\Gamma\types B}{\Gamma\types A\join B}\;\joinI2
    \and
    \inferrule{
      \Gamma\types A\join B \\ \Gamma,A \types C \\ \Gamma,B\types C
    }{\Gamma \types C}\;\joinE\\
    \inferrule{\Gamma,A\types B}{\Gamma\types A\To B}\;\ToI\and
    \inferrule{\Gamma\types A\To B \\ \Gamma\types A}{\Gamma\types B}\;\ToE
  \end{mathpar}
  \caption{Natural deduction for Heyting algebras}
  \label{fig:natded-heyting}
\end{figure}

For convenience, we collect all the rules of this modified \textbf{natural deduction for Heyting algebras} in \cref{fig:natded-heyting}.
Note that we change our notation and write $A\hom B$ as $A\To B$.

\begin{lem}\label{thm:heyting-strucadm}
  All the structural rules of exchange, weakening, and contraction are admissible in the natural deduction for Heyting algebras.
\end{lem}
\begin{proof}
  It will suffice to prove admissibility of the following rule, for any function $\sigma : \{1,\dots,m\} \to \{1,\dots,n\}$:
  \begin{mathpar}
    \inferrule*{A_{\sigma 1},\dots,A_{\sigma m} \types B}{A_1,\dots,A_n \types B}
  \end{mathpar}
  This is almost immediate from the fact that the premises of all rules have the same context as the conclusion, perhaps with a type added: regardless of how a derivation of ${A_{\sigma 1},\dots,A_{\sigma m} \types B}$ ends, we can apply the inductive hypothesis to its premises (perhaps passing to $\sigma\sqcup\idfunc : \{1,\dots,m+1\} \to \{1,\dots,n+1\}$) and then re-apply the final rule.

  The only exception is the rule $\idfunc$, for which we observe that if $A$ appears in the context $A_{\sigma 1},\dots,A_{\sigma m}$, then $A=A_{\sigma j}$ for some $1\le j\le m$, and hence $A=A_i$ for some $1\le i\le n$ (namely, $i=\sigma j$).
  Thus, we can also apply the same rule to obtain ${A_1,\dots,A_n \types A_i}$.
\end{proof}

\begin{lem}\label{thm:heyting-initial}
  The free Heyting algebra on a relational multigraph \cG can be described by the natural deduction for Heyting algebras.
\end{lem}
\begin{proof}
  Left to the reader.
  This will also follow as a special case of \cref{thm:stlc-initial}.
\end{proof}

The generalization to presentations is also easy.


\subsection{Natural deduction and logic}
\label{sec:natded-logic}

Let us now say a few words about what the natural deduction for Heyting algebras has to do with logic.
For a reader who thinks of logical connectives in terms of their action on truth values (e.g. ``if $A$ then $B$'' is true unless $A$ is true and $B$ is false), one way to make the connection to logic is to note that the poset of truth values
\[ \tv = \{ \mathrm{false} < \mathrm{true} \}\]
is a Heyting algebra, where the operations $\meet,\top,\join,\bot,\To$ correspond to ``and'', ``true'', ``or'', ``false'', and ``implies''.
(One way to see this easily is to identify $\tv$, up to equivalence, with the full subcategory of \bSet consisting of sets having at most one element.)

Now suppose \cG is a relational multigraph, or more generally a relational $(\meet,\join,\To)$-presentation.
We call the objects of \cG \textbf{propositional variables}.
Suppose furthermore that we have a map of relational multigraphs (or presentations) $\nu:\cG\to\tv$.
In other words, we assign a truth value to each propositional variable, in such a way that if $(A_1,A_2,\dots,A_n)\le B$ in \cG, and if $\nu(A_i)$ is true for all $i$, then also $\nu(B)$ is true.
Then by \cref{thm:natded-logic-initial} we have an induced map $\F\bHeyting\cG \to \tv$ of Heyting algebras.

The objects of $\F\bHeyting\cG$ are \emph{propositional formulas}, built out of the propositional variables by the operations $\meet,\top,\join,\bot,\To$ which we now regard as denoting the logical connectives ``and'', ``true'', ``or'', ``false'', and ``implies''.
Since $\F\bHeyting\cG \to \tv$ is a map of Heyting algebras, it extends the truth assignment $\nu$ to all such formulas by using the ``truth tables'' for all the connectives, e.g.\ $\nu(A\meet B)$ is true just when $\nu(A)$ and $\nu(B)$ are both true, etc.
Finally, the fact that $\F\bHeyting\cG \to \tv$ preserves inequalities means that if $A_1,\dots,A_n \types B$ is derivable in the natural deduction for Heyting algebras, and if $\nu(A_i)$ is true for all $i$, then also $\nu(B)$ is true.
% (where now the $A_i$ and $B$ are arbitrary formulas, not just propositional variables).

As a special case, if \cG is discrete (i.e.\ is nothing but a set of propositional variables), then any derivable judgment $\ec\types B$ exhibits the propositional formula $B$ as a \textbf{tautology}: a statement that becomes true \emph{whatever} truth values are substituted for its propositional variables.
For instance, here is a derivation exhibiting $(A\meet (B\join C)) \To ((A\meet B) \join (A\meet C))$ as a tautology:
\begin{mathpar}
  \tiny
  \let\mymeet\meet
  \def\meet{\mathord{\mymeet}}
  \let\myjoin\join
  \def\join{\mathord{\myjoin}}
  \inferrule*{
      \inferrule*{
        \inferrule*{\inferrule*{ }{A\meet (B\join C) \types A\meet (B\join C)
          }}{A\meet (B\join C) \types B\join C}\\
        \inferrule*{\inferrule*{
            \inferrule*{\inferrule{ }{
                  A\meet (B\join C),B\types A\meet (B\join C)
              }}{A\meet (B\join C),B \types A} \\
            \inferrule*{ }{
              A\meet (B\join C),B \types B}
          }{A\meet (B\join C),B \types A\meet B
        }}{A\meet (B\join C),B \types (A\meet B) \join (A\meet C)}\\
        \text{(and dually)}
        }{A\meet (B\join C)\types (A\meet B) \join (A\meet C)}
  }{\ec\types (A\meet (B\join C)) \To ((A\meet B) \join (A\meet C))}
\end{mathpar}
% VERSION WITH PRIMITIVE STRUCTURAL RULES:
% \begin{mathpar}
%   \tiny
%   \let\mymeet\meet
%   \def\meet{\mathord{\mymeet}}
%   \let\myjoin\join
%   \def\join{\mathord{\myjoin}}
%   \inferrule*{
%     \inferrule*{
%       \inferrule*{
%         \inferrule*{\inferrule*{ }{A\meet (B\join C) \types A\meet (B\join C)
%           }}{A\meet (B\join C) \types B\join C}\\
%         \inferrule*{\inferrule*{
%             \inferrule*{\inferrule*{\inferrule{ }{
%                   A\meet (B\join C)\types A\meet (B\join C)
%                 }}{A\meet (B\join C) \types A
%               }}{A\meet (B\join C),B \types A} \\
%             \inferrule*{\inferrule*{ }{
%                 B\types B
%               }}{A\meet (B\join C),B \types B}
%           }{A\meet (B\join C),B \types A\meet B
%         }}{A\meet (B\join C),B \types (A\meet B) \join (A\meet C)}\\
%         \text{(and dually)}
%         }{A\meet (B\join C),A\meet (B\join C)\types (A\meet B) \join (A\meet C)}
%     }{A\meet (B\join C)\types (A\meet B) \join (A\meet C)}
%   }{\ec\types (A\meet (B\join C)) \To ((A\meet B) \join (A\meet C))}
% \end{mathpar}
Thus, the natural deduction for Heyting algebras can be used as a means to derive tautologies in propositional logic.
More generally, if \cG has nontrivial relations (a.k.a.\ \emph{axioms}), then we can derive universally valid consequences of those axioms.

However, there is more to the relationship between type theory and logic than this.
There are many ways to derive tautologies, including methods such as simply plugging in all possible truth assignments for the propositional variables and checking that the formula is always true.
But the natural deduction for Heyting algebras has the important property that it (at least roughly) \emph{mirrors the process of ordinary informal mathematical reasoning}.

It is easiest to see this if we reformulate the theory a little.
Let us omit the contexts ``$\Gamma\types$'' from all judgments in a derivation tree, instead writing simply the consequent $A$.
In place of the $\idfunc$ rule deriving $\Gamma\types A$, we write simply ``$A$'' without any justification, and call it a \emph{hypothesis}.
Finally, when a type $A$ is removed from the context on our way down the tree, we cross off that hypothesis everywhere that it appears above, and say that the hypothesis has been \emph{discharged}.
At the end, the set of remaining hypothesis is the antecedent of the conclusion; if no hypotheses remain undischarged, we have derived a tautology.

For instance, the above derivation of the distributive law would be written in this style as
\begin{mathpar}
  \inferrule*[Right=$\ToI$]{
    \inferrule*[Right=$\joinE$]{
      \inferrule*{\cancel{A\meet (B\join C)}}{B\join C}\\
      \inferrule*{\inferrule*{
        \inferrule*{\cancel{A\meet (B\join C)}}{A}\\
        \cancel{B}
        }{A\meet B}}{(A\meet B)\join (A\meet C)}\\
      \inferrule*{\inferrule*{
        \inferrule*{\cancel{A\meet (B\join C)}}{A}\\
        \cancel{C}
        }{A\meet C}}{(A\meet B)\join (A\meet C)}\\
    }{(A\meet B)\join (A\meet C)}
  }{(A\meet (B\join C))\To ((A\meet B)\join (A\meet C))}
\end{mathpar}
Note that there is some ambiguity; it is not obvious from looking at the derivation which rule caused which hypothesis to be discharged.
In the above example, the hypotheses $B$ and $C$ are discharged by the $\joinE$ rule, while the hypothesis ${A\meet (B\join C)}$ (everywhere it appears) is discharged by the $\ToI$ rule.
Sometimes people annotate the discharges in some way to indicate this.

However, the real point of a representation like this is that the \emph{process of writing it}, from the top down, is supposed to mirror the process of informal reasoning.
First we assume $A\meet (B\join C)$, and deduce from it both $A$ and $B\join C$.
Then we use $B\join C$ by additionally assuming $B$ and $C$ in two separate cases (sub-derivations), and in each of those cases we separately deduce ${(A\meet B)\join (A\meet C)}$ (by way of $A\meet B$ and $A\meet C$ respectively).
Thus, completing those cases (and ending our assumptions of $B$ and $C$) we have $(A\meet B)\join (A\meet C)$.
Finally, ending our assumption of $A\meet (B\join C)$, we have $(A\meet (B\join C))\To ((A\meet B)\join (A\meet C))$.

From this perspective, the rules in \cref{fig:natded-heyting} can also be glossed in the language of ``proof strategies''.
For instance, $\meetI$ says that ``to prove $A\meet B$, it suffices to prove $A$ and $B$ separately'', while $\ToE$ says that ``if we know $A\To B$, and we also know $A$, then we can conclude $B$'' (the rule of \textit{modus ponens}).
We encourage the reader to similarly gloss the other rules.

While it is arguable whether this \emph{exactly} mirrors the process of informal reasoning, it certainly has a close kinship with it --- much closer than the production of tautologies by checking all possible truth assignments.
In particular, it includes one essential aspect of informal reasoning: the ability to \emph{reason under a temporary assumption} and then ``discharge'' that assumption in reaching some other conclusion.
This sort of \emph{hypothetical reasoning} is central to everyday mathematics, so the fact that it also appears in natural deduction logic is a strong argument in favor of the ``naturalness'' of the latter.

This is the real origin of the name ``natural deduction''.
In fact, historically, this representation with discharged hypotheses came first, and only later was it rewritten to carry along the context, and then generalized to theories without contraction and weakening.
Other systems of formal logic, such as ``Hilbert-style calculi'' (see \cref{ex:hilbert}), though they can derive the same class of tautologies, do not really include hypothetical reasoning as such, and hence do not model informal reasoning as well.

\begin{rmk}
  [TODO: Frobenius/Hopf for $\join$, for reasoning with extra hypotheses, and distributivity without $\To$.]
\end{rmk}

Now, it may seem that the logical expressivity of the natural deduction for Heyting algebras is lacking because there is no operation corresponding to \emph{negation}.
However, we can do pretty well by defining $\neg A$ to mean $A\To\bot$, so that its rules are
\begin{mathpar}
  \inferrule{\Gamma,A\types\bot}{\Gamma\types \neg A}\and
  \inferrule{\Gamma\types \neg A \\ \Gamma\types A}{\Gamma\types \bot}
\end{mathpar}
In other words, to prove $\neg A$, it suffices to show that assuming $A$ leads to a contradiction, while if we have both $\neg A$ and $A$ we obtain a contradiction.
Using these rules, here is a derivation of one of ``de Morgan's laws'' as a tautology:
\begin{mathpar}
  \small
  \inferrule*{
    \inferrule*{
      \inferrule*{\inferrule*{
        \inferrule*{ }{\neg(A\join B),A \types \neg(A\join B)}\\
        \inferrule*{\inferrule*{ }{\neg(A\join B),A \types A}}{\neg(A\join B),A \types A\join B}
        }{\neg(A\join B),A \types \bot
        }}{\neg(A\join B) \types \neg A}\\
      \text{(and dually)}
      }{\neg(A\join B) \types \neg A\meet \neg B}
  }{\ec\types \neg(A\join B)\To(\neg A\meet \neg B)}
\end{mathpar}
% VERSION WITH PRIMITIVE STRUCTURAL RULES
% \begin{mathpar}
%   \tiny
%   \let\mymeet\meet
%   \def\meet{\mathord{\mymeet}}
%   \let\myjoin\join
%   \def\join{\mathord{\myjoin}}
%   \let\myTo\To
%   \def\To{\mathord{\myTo}}
%   \inferrule*{
%     \inferrule*{
%       \inferrule*{\inferrule*{
%           \inferrule*{ }{(A\join B)\To\bot \types (A\join B)\To\bot}\\
%           \inferrule*{\inferrule*{ }{A\types A}}{A\types A\join B
%           }}{(A\join B)\To\bot,A \types \bot
%         }}{(A\join B)\To\bot \types A\To\bot}\\
%       \inferrule*{\inferrule*{
%           \inferrule*{ }{(A\join B)\To\bot \types (A\join B)\To\bot}\\
%           \inferrule*{\inferrule*{ }{B\types B}}{B\types A\join B
%           }}{(A\join B)\To\bot,B \types \bot
%         }}{(A\join B)\To\bot \types B\To\bot}
%       }{(A\join B)\To\bot \types (A\To\bot)\meet (B\To\bot)}
%   }{\ec\types ((A\join B)\To\bot)\To((A\To\bot)\meet (B\To\bot))}
% \end{mathpar}
However, not \emph{every} tautology can be derived this way.
In particular, $\neg\neg A \To A$ (the ``law of double negation'') and $A\join \neg A$ (the ``law of excluded middle'') are not derivable, because although they hold in $\tv$, their analogues fail to hold in other Heyting algebras.
(In fact, they hold in a Heyting algebra exactly when that Heyting algebra is a \emph{Boolean} algebra; see \cref{ex:heyt-bool}.)
Thus, although we have something that ``looks like logic'', it is not exactly classical logic.

One way to resolve this is to simply add another rule, such as the following for ``proof by contradiction'':
\begin{mathpar}
  \inferrule*{\Gamma,\neg A\types \bot}{\Gamma\types A}
\end{mathpar}
(The rule for $\neg A$ derived from $\To$ is the form of ``proof by contradiction'' where we prove a statement is \emph{false} by assuming it is true and deriving a contradiction; here we are considering the opposite form where we prove a statement to be \emph{true} by assuming it to be false and deriving a contradiction.)
This mirrors the process of informal reasoning in classical mathematics fairly closely, though it is a bit problematic from a type-theoretic perspective (e.g.\ it fails the principles enunciated in \cref{sec:why-multicats}).
As we will see in \cref{chap:polycats}, one can also formulate a well-behaved type theory that it \emph{can} prove all classical tautologies, by restoring the left/right and $\meet/\join$ symmetries.

However, it is also valuable to observe that conversely, if we are willing to generalize our notion of ``logic'', we obtain something much more generally applicable.
Indeed, this is really the whole point of categorical logic, as put forward in \cref{sec:intro}: we can apply ``set-like'' reasoning to objects of arbitrary categories as long as we are careful about what sort of reasoning we use.

So far, we have applied this principle mainly to equational reasoning about different kinds of terms.
However, we now have a type theory that is powerful enough to codify significant amounts of mathematical reasoning (though not yet anything involving quantifiers such as ``for all'' and ``there exists''; that will come in \cref{chap:fol}).
Thus, we can lift our notion of ``generalized logic'' back to informal mathematical reasoning.
It takes a bit of practice to learn to write informal mathematical proofs that could (at least in principle) be codified in such a generalized logic, but it is eminently possible.
(It is much \emph{more} possible because, as discussed above, our ``generalized logic'' is expressed in a style that already closely mirrors ordinary mathematical reasoning; we simply have to learn which familiar styles of argument are valid in what situations.)

The payoff is that the result is much more general than it appears, since it is true ``internally to any Heyting algebra''.
By contrast, ordinary (``classical'') mathematical reasoning is only valid in \emph{Boolean} algebras (see \cref{ex:heyt-bool}).
Lest the reader think that Heyting algebras seem esoteric, we point out that the lattice of open subsets of any topological space is a Heyting algebra (\cref{ex:frames}).

\begin{rmk}\label{rmk:soundness-completeness}
  In the context of logic, the initiality theorem (\cref{thm:heyting-initial}) corresponds to what are traditionally called \emph{soundness} and \emph{completeness} theorems.
  A \emph{soundness} theorem says informally ``if something is provable, then it is true in all models''.
  This follows from \cref{thm:heyting-initial} because the inequalities in a free Heyting algebra are exactly those that are provable (i.e.\ derivable) in the type theory; thus, if something is provable, then it is true in the free Heyting algebra, and therefore also in every other Heyting algebra.
  Dually, a \emph{completeness} theorem says informally ``if something is true in all models, then it is provable''.
  This also follows from \cref{thm:heyting-initial} because if something is true in all Heyting algebras, then it is in particular true in a free Heyting algebra; and hence, by our construction of the latter, it is provable in the type theory.
\end{rmk}

The ``generalized logic'' corresponding to Heyting algebras is called \textbf{intuitionistic} or \textbf{constructive logic}, because of its similarity to the mathematics advocated by certain mathematicians calling themselves ``intuitionist'' or ``constructive'' in the early 20th century.
While we are stuck with these labels, it is probably best (for a classically trained category theorist first encountering the notion) not to read too much into them.
The point is simply that we make our mathematics more general by generalizing our logic, and this is the logic that corresponds naturally to cartesian closed lattices, which are certainly a categorically natural notion.

The observation that the logical operations of ``and'', ``or'', ``if-then'', and so on in the poset $\tv$ have the same universal properties (and hence can be represented by the same type operations) as the operations $A\times B$, $A+B$, $B^A$ in the category \bSet has a distinguished pedigree and many names: \emph{propositions as types}, \emph{proofs as terms}, or the \emph{Curry--Howard correspondence} (see~\cite{wadler:pat} for some history).
As we will see, this correspondence is also central to the use of dependent type theory (\cref{chap:dtt}) as a foundation for mathematics.
Some ``constructivist'' mathematicians have argued that this correspondence should determine the \emph{meanings} of the logical operations in terms of proofs --- that is, a proof of ``$P$ and $Q$'' should be a pair $(p,q)$ where $p$ is a proof of $P$ and $q$ is a proof of $Q$; a proof of ``if $P$ then $Q$'' should be a function transforming any proof of $P$ into a proof of $Q$; and so on.
This is sometimes called the \emph{Brouwer--Heyting--Kolmogorov (BHK) interpretation}.
However, we will have little to say about the philosophical side of constructive logic.

In any case, having made these observations in the case of \emph{cartesian} closed lattices, it is natural to entertain similar ideas for other values of \fS.
Roughly speaking, the names of the corresponding ``generalized logics'' are:
\begin{center}
\begin{tabular}{c|c}
  $\fS$ & generalized logic\\\hline
  cartesian & intuitionistic logic\\
  symmetric & linear logic\\
  semicartesian & affine logic\\
  relevance & relevance logic
\end{tabular}
\end{center}
To be precise, we are currently talking about variants of all these logics that should be qualified as ``intuitionistic''; there are also ``classical'' versions of linear, affine, and relevance logics in which the laws of double negation and excluded middle hold.
Moreover, at least in the linear case one should also add a phrase like ``multiplicative-additive''\footnote{In the lingo of linear logic, $\tensor$ is a ``multiplicative'' connective, while $\meet$ and $\join$ are ``additive''.
  Classical linear logic also includes another multiplicative connective called $\parr$ that is dual to $\tensor$ in the same way that $\join$ is dual to $\meet$; see \cref{sec:cllin}.} to describe our current theory, because the name ``linear logic'' usually refers to a system with some additional modalities. % (see [TODO]).
Furthermore, at this point all of them should have the prefix ``propositional'', since we are not yet considering quantifiers of any sort (``there exists'' and ``for all'').

The name ``linear logic'' comes from the same intuition as our use of ``linearity'' to describe \cref{thm:multicat-linear}.
The name ``affine logic'' is similarly inspired by the fact that while a linear transformation $T(\vec v) = A\vec v$ must use its argument exactly once in each term, an affine transformation $T(\vec v) = A\vec v + \vec b$ also has terms that do not use its argument at all.
Both of these logics are primarily studied by computer scientists; the distinction between $\tensor$ and $\meet$ can be interpreted in terms of ``resource usage'' (but that is far beyond our scope here).

Finally, ``relevance logic'' was invented by some philosophers seeking to avoid certain facts about implication that they regarded as ``paradoxical'' because their ``if'' parts are not ``relevant'' to their ``then'' parts, such as $A\To (B\To A)$.
The straightforward derivation of this tautology in our type theory requires weakening:
\begin{mathpar}
  \inferrule*{\inferrule*{\inferrule*[Right=weakening]{A\types A}{A,B\types A
      }}{A\types (B\To A)
    }}{\ec\types A\To (B\To A)}
\end{mathpar}
and in fact the type theory for closed relevance monoidal lattices cannot derive $\ec\types A\hom (B\hom A)$ (although this is not obvious; see \cref{ex:relevance-eg,ex:seqcalc-logic}).

The most commonly used relevance logics satisfy other principles that our type theory does not, notably the distributive law $A\meet (B\join C) \cong (A\meet B)\join (A\meet C)$ (note that our derivation of this above also used weakening).
Of course, any closed monoidal lattice satisfies the distributive law $A\tensor (B\join C) \cong (A\tensor B)\join (A\tensor C)$, but as we have observed, both weakening and contraction are necessary to force $\tensor$ to coincide with $\meet$.
(It is possible to formulate type theories that ensure the $\meet/\join$ distributive law as well, but this requires a fancier notion of generalized multicategory.) %, so we postpone it to [TODO].


% \subsection{Sequent calculus and logic}
% \label{sec:seqcalc-logic}

% [TODO: take out of \cref{ex:seqcalc-logic}.  Need to build in cuts on both sides of axioms in general, as mentioned in \cref{sec:unary-theories}.]


\subsection*{Exercises}

\begin{ex}\label{ex:cart-typetheory}
  Prove \cref{thm:semicart-multicat-repr,thm:cart-multicat-repr} using our posetal type theories.
  Specifically:
  \begin{enumerate}
  \item If we have exchange and weakening, prove that $\one \cong \top$.
  \item If we have exchange, weakening, and contraction, prove that $A\tensor B \cong A\times B$.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:nnlem}
  Prove that $\neg\neg(P\join\neg P)$ is an intuitionistic tautology, i.e.\ construct a derivation of $\ec\types\neg\neg(P\join\neg P)$ in the natural deduction for Heyting algebras.
\end{ex}

\begin{ex}\label{ex:heyt-bool}
  Prove that the following are equivalent for a Heyting algebra:
  \begin{enumerate}
  \item The law of excluded middle $P\join\neg P$ is true, i.e.\ $P\join\neg P$ is the top element for all $P$.
  \item The law of double negation $\neg\neg P\To P$ is true.
  \item The Heyting algebra is a Boolean algebra, i.e.\ every element $P$ has a ``complement'' $\Pbar$ such that $P\meet\Pbar = \bot$ and $P\join\Pbar = \top$.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:demorgan}
  Of the four ``de Morgan's laws'', three are intuitionistic tautologies and one is not.
  Construct derivations of three of the following sequents in the natural deduction for Heyting algebras:
  \begin{align*}
    \neg(P\join Q) &\types \neg P \meet \neg Q\\
    \neg(P\meet Q) &\types \neg P \join \neg Q\\
    \neg P \meet \neg Q &\types \neg(P\join Q)\\
    \neg P \join \neg Q &\types \neg(P\meet Q)
  \end{align*}
\end{ex}

\begin{ex}\label{ex:frames}
  A \textbf{frame} is a lattice with infinitary joins satisfying the infinite distributive law $A \meet \left(\bigjoin_i B_i\right) \cong \bigjoin_i (A\meet B_i)$.
  \begin{enumerate}
  \item Prove that any (small) frame is a Heyting algebra.
  \item Prove that the lattice of open sets of any topological space is a frame.
  \item Describe a type theory for frames.  This is called (propositional) \textbf{geometric logic}.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:not-lem}
  Give concrete examples of Heyting algebras satisfying the following:
  \begin{enumerate}
  \item There is an element $P$ for which $P\join \neg P$ is not the top element.
  \item There are elements $P$ and $Q$ for which the fourth de Morgan's law (see \cref{ex:demorgan}) does not hold.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:relevance-eg}
  Describe a concrete example of a closed relevance monoidal lattice containing two objects $A$ and $B$ such that there is no morphism from $\one$ (the unit object) to $A\hom (B\hom A)$.
  Deduce that $\ec\types A\hom (B\hom A)$ is not derivable in the type theory for closed relevance monoidal lattices.
\end{ex}

\begin{ex}\label{ex:seqcalc-logic}
  One of the advantages of sequent calculus over natural deduction is that because all of its rules \emph{introduce} operations on the left or the right, it is easier to conclude underivability theorems.
  \begin{enumerate}
  \item Define a sequent calculus for closed \fS-monoidal lattices, and prove the cut admissibility and initiality theorems.
  \item Prove that $\ec\types A\hom (B\hom A)$ is not derivable in the sequent calculus for closed relevance monoidal lattices, by ruling out all possible ways that such a derivation could end.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:hilbert}
  TODO: A whole section on this?  There should be a general notion of ``closed category'' for any suitable kind of multicategory, with a resulting combinatory logic and hilbert system.
  \url{https://nforum.ncatlab.org/discussion/4632/closed-category/}

  Another way of deriving tautologies is called a \textbf{Hilbert system}.
  A Hilbert system can be formulated as a sort of type theory where the judgments all have empty context, i.e.\ are of the form $\types A$ where $A$ is a propositional formula.
  Instead of the ``modular'' left/right rules of sequent calculus or the introduction/elimination rules of natural deduction, where the rules for each connective do not refer to any other connective, a Hilbert system gives a special place to implication $\To$.
  The \emph{only} rule with premises\footnote{Hilbert systems for more complicated logics have one or two more rules with premises, but in general there are very few.} is the empty-context form of $\ToE$, \emph{modus ponens}:
  \[ \inferrule{\types A\To B \\ \types A}{\types B} \]
  The behavior of all other connectives is specified by \emph{axioms} (rules with no premises, other than the well-formedness of the formulas appearing in them).
  For instance, we complete the description of $\To$ with the following axioms:
  \begin{mathpar}
    \inferrule{\types A\type}{\types A\To A}\and
    \inferrule{\types A\type \\ \types B\type}{\types A\To (B\to A)}\and
    \inferrule{\types A\type \\ \types B\type \\ \types C\type}{\types (A\To (B\To C)) \To ((A\To B)\To (A\To C))}
  \end{mathpar}
  The axioms for the remaining connectives are (omitting the obvious premises and the $\types$):
  \begin{mathpar}
    A\To (B\To (A\meet B))\and
    (A\meet B)\To A\and
    (A\meet B)\To B\\
    A\To (A\join B)\and
    B\To (A\join B)\and
    (A\To C)\To ((B\To C) \To ((A\join B)\To C))\\
    A\To \top\and
    \bot \To A
  \end{mathpar}
  Prove that this Hilbert system derives exactly the same tautologies as the natural deduction for Heyting algebras.

  (The main reasons for using a Hilbert system seem to be that it \emph{never} changes the context and has very few rules.
  This sometimes makes metatheoretic arguments easier, but at the cost of greater distance from informal mathematics, since as we have remarked the latter gives a central place to hypothetical reasoning.
  It should also be noted that the symbol $\types$ is often used differently in the context of Hilbert systems; rather than $\types$ being part of each judgment, the notation ``$\Gamma\types A$'' means that we can derive $A$ (that is, $\types A$ in our notation) in the Hilbert system augmented by all the formulas in $\Gamma$ as additional axioms.)
\end{ex}

\begin{ex}\label{ex:cocartesian-typetheory}
  Is there a well-behaved type theory (i.e.\ having admissible cut and an initiality theorem) corresponding to the (posetal version of the) ``cocartesian multicategories'' of \cref{ex:cocartesian-clubs}?
  \textit{(As of this writing, the answer is not known to the author.)}
\end{ex}



\section{Simply typed $\lambda$-calculus}
\label{sec:stlc}

We now move back up the ladder from posets to categories.
In this case it becomes more important to adhere to principle~\eqref{princ:adm} and make our structural rules admissible.
Otherwise our derivations would become polluted with applications of these rules, and our terms (which, as ever, we want to be simply syntax for derivations) would be likewise quite messy-looking.
We have already seen in \cref{thm:heyting-strucadm} that the structural rules can be made admissible in the cartesian case where we want all of them, so we consider that case first.
In addition to being the easiest, this is probably also the most commonly used case.

We begin by introducing terms for the rules from \cref{sec:heyting-algebras}, as shown in \cref{fig:stlc}.
As in \cref{sec:heyting-algebras}, we omit $\tensor$ and $\unit$ since they coincide with $\meet$ and $\top$.
We also switch back to categorical notations $\times,\unit,+,\zero$ instead of $\meet,\top,\join,\bot$.
We also write $A\to B$ instead of $A\hom B$; this has the pleasing consequence that the term syntax $M:A\to B$ looks the same as the common mathematical notation for functions.

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{\types A\type \\ (x:A)\in \Gamma}{\Gamma\types x:A}\;\idfunc
    \and
    \inferrule{f\in \cG(A_1,\dots,A_n;B) \\ \Gamma\types M_1:A_1 \\ \dots \\ \Gamma \types M_n:A_n}{\Gamma\types f(M_1,\dots,M_n):B}\;f
    \and
    \inferrule{\Gamma\types M:A \\ \Gamma\types N:B}{\Gamma\types \pair{M}{N} :A\times B}\;\timesI
    \and
    \inferrule{\Gamma\types M:A\times B}{\Gamma\types \pr1AB(M):A}\;\timesE1
    \and
    \inferrule{\Gamma\types M:A\times B}{\Gamma\types \pr2AB(M):B}\;\timesE2
    \\
    \inferrule{ }{\Gamma\types \ttt:\unit}\;\unit I
    \and
    \inferrule{\Gamma\types M:\zero}{\Gamma\types \abort(M):C}\;\zero E
    \\
    \inferrule{\Gamma\types M:A}{\Gamma\types \inl(M):A+B}\;\plusI1
    \and
    \inferrule{\Gamma\types N:B}{\Gamma\types \inr(N):A+B}\;\plusI2
    \and
    \inferrule{
      \Gamma\types M:A+B \\ \Gamma,u:A \types P:C \\ \Gamma,v:B\types Q:C
    }{\Gamma \types\acase AB(M,u.P,v.Q):C}\;\plusE
    \and
    \inferrule{\Gamma,x:A\types M:B}{\Gamma\types \lambda x.M:A\to B}\;\toI\and
    \inferrule{\Gamma\types M:A\to B \\ \Gamma\types N:A}{\Gamma\types M N:B}\;\toE
  \end{mathpar}
  \caption{The simply typed $\lambda$-calculus with products and coproducts}
  \label{fig:stlc}
\end{figure}

Most of the term annotations should be familiar from \cref{sec:multicat-prod-coprod}; indeed they are even simpler, since the (expected) presence of the structural rules allows us to omit some of the more verbose annotations.
The rule $\toI$ introduces a new kind of term, a \textbf{$\lambda$-abstraction}.
Since the variable $x$ appears in the premise but not the conclusion, it must be bound in the resulting term; there is nothing else to say, so we simply prefix the letter $\lambda$ to indicate the rule.
Intuitively, we think of $\lambda x.M$ as meaning ``the function that takes one argument, called $x$, and returns the value of $M$ (which includes $x$)''.
For instance, $\lambda x.x^2$ denotes the function that squares its argument, $\lambda x.(x+3)$ denotes the function that adds three to its argument, and so on.
Because of the importance of this operation, the type theory of \cref{fig:stlc}, which we expect to correspond to cartesian closed categories with coproducts, is called the \textbf{simply typed $\lambda$-calculus (STLC) with products and coproducts}.
(The unqualified ``STLC'' would omit the rules for $\times,\unit,+,\zero$.)

The term annotation for the rule $\toE$ simply ``pairs up'' two terms, one of which has type $A\to B$ and one of which has type $A$.
Intuitively, we are ``applying'' a function $M:A\to B$ to an argument $N:A$.
Technically there ought also to be a label indicating the rule being applied to pair these terms up, such as $\fapp(M,N)$.
However, any system of notation has room for \emph{one} operation denoted by simple juxtaposition (e.g.\ in high-school algebra it is multiplication, while in group theory it is the group operation), and the importance of the type operation $\to$ leads us to choose $\toE$ for this honor in type theory.
Most mathematicians write $f(a)$ for the application of a function $f$ to an argument $a$; since parentheses are used as usual for grouping, this notation is also valid here, just as $(x)(y)=xy$ in high-school algebra.

% TODO: with "types as input" the way we are doing it here, application actually has to be annotated with the argument type $A$ for type-checking to work as it usually has so far.

\begin{lem}\label{thm:stlc-uniqderiv}
  If a term $\Gamma\types M:A$ is derivable in the simply typed $\lambda$-calculus, then it has a unique derivation.
\end{lem}
\begin{proof}
  This is almost immediate.
  Since the premises of all rules have the same context as the conclusion, perhaps with a type added, there is no ambiguity about how to split things up, and hence no need for the uglier annotations used in \cref{sec:multicat-prod-coprod}.
\end{proof}

\begin{lem}\label{thm:stlc-strucadm}
  The structural rules of exchange, contraction, and weakening are admissible in the simply typed $\lambda$-calculus.
  Moreover, they make the derivations into a cartesian multigraph (i.e.\ they are functorial as in \cref{defn:fS-multicategory}).
\end{lem}
\begin{proof}
  The proof is essentially the same as \cref{thm:heyting-strucadm}, carrying along terms and variables; we prove the following rule, for any function $\sigma : \{1,\dots,m\} \to \{1,\dots,n\}$:
  \begin{mathpar}
    \inferrule*{y_1:A_{\sigma 1},\dots,y_m:A_{\sigma m} \types M:B}{x_1:A_1,\dots,x_n:A_n \types \sigma^*M:B}
  \end{mathpar}
  by pushing up through all rules until we get to $\idfunc$.
  Regarded as an operation on terms, $\sigma^*$ is defined by the clause
  \begin{align*}
    \sigma^*y_j &= x_{\sigma j}\\
    \intertext{along with trivial ``descending into subterms'' clauses for all other terms, such as}
    \sigma^*\pair M N &= \pair{\sigma^*M}{\sigma^*N}\\
    \sigma^*\case(M,u.P,v.Q) &= \case(\sigma^*M, u.(\sigma\sqcup\idfunc)^*P,v.(\sigma\sqcup\idfunc)^*Q)
  \end{align*}
  and so on.
  Intuitively, we simply substitute the variable $x_{\sigma j}$ for $y_j$ wherever it appears, for all $1\le j\le m$.
  A similar induction proves that this operation is functorial, yielding a cartesian multigraph.
\end{proof}

In fact, if $\sigma$ is injective --- that is, it is composed of exchange and weakening only --- and if we choose variables $y_j = x_{\sigma j}$ (which is only possible if $\sigma$ is injective), then in fact $\sigma^*M = M$.
For instance, we have
\[ x:A, y:B \types \pair x y : A\times B\]
and by exchange and weakening we can obtain also
\[ y:B, z:C, x:A \types \pair x y : A\times B.\]
with the same term $\pair x y$.
This does not contradict ``terms are derivations'', because we only require a term to determine a unique derivation \emph{when paired with its context and consequent}.

\begin{rmk}
  As remarked briefly at the beginning of the section, the admissibility of the structural rules is central to having a clean theory of terms and a clean proof of the initiality theorem.
  If we took the structural rules as primitive, then to maintain ``terms as derivations'' we would have to include information about the structural rules in terms, for instance annotating the derivation
  \[ \inferrule*{\inferrule*{A,B\types A \\ A,B\types B}{A,B\types A\times B}}{B,A\types A\times B}\]
  with a term like $y:B,x:A\types \sigma^*\pair{x}{y}:A\times B$, distinguishing it from the \emph{different} derivation
  \[ \inferrule*{B,A\types B \\ B,A\types A}{B,A\types A\times B}\]
  that we could write as $y:B,x:A\types \pair{x}{y}:A\times B$.
  Clearly these two derivations ought to have the same term.
  However, if structural rules are primitive, then using the same term for both of them would break the ``terms as derivations'' principle.
  If we did this, then to prove the initiality theorem using terms, after inducting over derivations we would have to prove that the interpretation of a term is independent of its derivation.
  This sort of thing is difficult and tedious, and hence often left to the reader or left unmentioned altogether.
  Making the structural rules admissible avoids both horns of the dilemma.
\end{rmk}

Now we need substitution.
Since all our other rules maintain the same context, it is natural to do the same here.

\begin{lem}\label{thm:stlc-subadm}
  Substitution is admissible in the simply typed $\lambda$-calculus: given derivations of $\Gamma\types M:A$ and $\Gamma,x:A\types N:B$, we can construct a derivation of $\Gamma\types M[N/x]:B$.
\end{lem}
\begin{proof}
  By induction on the derivation of $\Gamma,x:A\types N:B$, as usual.
  There are two mildly new features.
  Firstly, since the contexts are maintained rather than split, we have to recurse into \emph{all} premises of each rule.
  Secondly, when we get down to $\idfunc$ we might find a variable other than $x$, in which case there is no substitution to do.
  Thus the clauses defining substitution are as shown in \cref{fig:stlc-sub}.
  As in \cref{sec:multicat-moncat,sec:multicat-prod-coprod}, to write substitution using terms, we need to ensure by $\alpha$-equivalence that the bound variables $u,v$ in $\case$ and $y$ in $\lambda$ do not appear free in $M$.
\end{proof}

\begin{figure}
  \centering
  \begin{align*}
    x[M/x] &= M \\
    y[M/x] &= y \qquad (y\text{ a variable } \neq x)\\
    f(N_1,\dots,N_n)[M/x] &= f(N_1[M/x],\dots,N_n[M/x])\\
    \pair{P}{Q}[M/x] &= \pair{P[M/x]}{Q[M/x]}\\
    \pi_1(N)[M/x] &= \pi_1(N[M/x])\\
    \pi_2(N)[M/x] &= \pi_2(N[M/x])\\
    \ttt[M/x] &= \ttt\\
    \abort(N)[M/x] &= \abort(N[M/x])\\
    \inl(N)[M/x] &= \inl(N[M/x])\\
    \inr(N)[M/x] &= \inr(N[M/x])\\
    \case(N,u.P,v.Q)[M/x] &= \case(N[M/x],u.P[M/x],v.Q[M/x])\\
    (\lambda y.N)[M/x] &= \lambda y.N[M/x]\\
    (PQ)[M/x] &= (P[M/x])(Q[M/x])
  \end{align*}
  \caption{Substitution in simply typed $\lambda$-calculus}
  \label{fig:stlc-sub}
\end{figure}

Note that the contraction rule is actually a special case of substitution, namely the substitution of one variable for another.
That is, given $\Gamma,x:A,y:A \types M:B$, we have $\Gamma,x:A \types M[x/y]:B$ which is (by induction, if you wish) equal to the contraction of $M$ obtained from \cref{thm:stlc-strucadm}.

The natural sort of ``associativity'' for this kind of substitution is also different: it combines the ``associativity and interchange'' properties in one, since if a variable $y$ is free in $N[M/x]$ then it might appear in \emph{both} $M$ and $N$.

\begin{lem}\label{thm:stlc-subassoc}
  Given derivations of $\Gamma\types M:A$ and $\Gamma,x:A\types N:B$ and $\Gamma,x:A,y:B\types P:C$, we have
  \[ P[N/y][M/x] = P[M/x][N[M/x]/y]. \]
\end{lem}
On the left-hand side, $P[N/y][M/x]$ means $(P[N/y])[M/x]$.
On the right-hand side, when writing $P[M/x]$ we have technically to apply weakening to $M$ (by \cref{thm:stlc-strucadm}) so that it has context $\Gamma,y:B$ first.
\begin{proof}
  A straightforward induction on derivations.
  For the ``base cases'' of variables, we have
  \begin{align*}
    x[N/y][M/x] &= x[M/x]\\
                &= M \\
                &= M[N[M/x]/y]\tag{*}\\
                &= x[M/x][N[M/x]/y]\displaybreak[0]\\
    y[N/y][M/x] &= N[M/x]\\
                &= y[N[M/x]/y]\\
                &= y[M/x][N[M/x]/y]\displaybreak[0]\\
    z[N/y][M/x] &= z[M/x]\\
                &= z\\
                &= z[M/x]\\
                &= z[M/x][N[M/x]/y]
  \end{align*}
  where $z\neq x,y$.
  The equality (*) is because $y$ does not appear in $M$, i.e.\ $M$ has been obtained by weakening from a context not including $y$ as remarked above.
  (Formally, we ought to prove by a further induction that substituting for a variable obtained by weakening never changes the term/derivation.)
\end{proof}

We also need to know that substitution commutes with the other structural rules.
For weakening and exchange this is immediate from the observation that these rules do not change the term.
For contraction, it follows from \cref{thm:stlc-subassoc} and the observation that contraction is a special case of substitution:
\begin{gather}
  N[x/y][M/x] = N[M/x][x[M/x]/y] = N[M/x][M/y].\label{eq:sub-contr-1}\\
  N[M/x][y/z] = N[y/z][M[y/z]/x]\label{eq:sub-contr-2}
\end{gather}

Now we can state the $\beta$- and $\eta$-conversion rules.
Those for products and coproducts are the familiar ones from \cref{fig:moncat-prod-coprod-equiv}.
The $\beta$-conversion rule for $\to$:
\[ (\lambda x.M)N \equiv M[N/x]\]
says that if we apply a function defined by $\lambda$-abstraction to an argument, the result is what we get by ``plugging in'' the argument to the expression defining the function.
That is, if $f(x)=x^2$ then $f(3) = 3^2$.
The $\eta$-conversion rule says that any function is a $\lambda$-abstraction:
\[  M \equiv \lambda x.Mx \qquad \text{if } M:A\to B\]
A straightforward induction shows that $\equiv$ is a congruence not only for substitution, but also for the new admissible structural rules from \cref{thm:stlc-strucadm}.

Now we are ready to prove the initiality theorem.
Note that we generate our free structure from a mere multigraph, not (as one might guess) a cartesian multigraph.
A cartesian multigraph contains operations and equations, so to use it as base data we would need to incorporate those operations into $\equiv$.

\begin{thm}\label{thm:stlc-initial}
  The free cartesian closed category with coproducts generated by a multigraph \cG can be presented by the simply typed $\lambda$-calculus under \cG: its underlying cartesian multigraph is that constructed in \cref{thm:stlc-strucadm} modulo $\equiv$, and its composition is given by substitution.
\end{thm}
\begin{proof}
  Although \cref{thm:stlc-subadm,thm:stlc-subassoc} are not stated in the usual form of multicategory composition operations, we can easily derive those operations from them.
  Given $\Gamma\types M:A$ and $\Delta,x:A,\Psi\types N:B$, we can apply weakening and exchange to obtain $\Delta,\Gamma,\Psi\types M:A$ and $\Delta,\Gamma,\Psi,x:A\types N:B$; then \cref{thm:stlc-subadm} yields $\Delta,\Gamma,\Psi\types N[M/x]:B$.
  Associativity and interchange are the special cases of \cref{thm:stlc-subassoc} where $x$ does not occur in $P$ and where $x$ does not occur in $N$, respectively, and the identity laws follow as usual.
  Thus to have a cartesian multicategory it remains to check \cref{defn:fS-multicategory}\ref{item:cartmulti-3} and \ref{item:cartmulti-4}, using in particular~\eqref{eq:sub-contr-1} and~\eqref{eq:sub-contr-2}.
  We leave this to the reader in \cref{ex:stlc-cartmulti}; it can be done directly or by way of \cref{ex:cartmulti-oneplace}.

  The rules for all the type operations give this cartesian multicategory products, coproducts, and closed structure; thus it underlies a cartesian closed category with coproducts.
  Initiality follows as usual: given a map of multigraphs $P:\cG\to \cM$, where \cM is a cartesian closed category with coproducts, we extend $P$ to all types by induction, then define it on all derivations by induction, then check that $\equiv$ is preserved by induction.
  As always, this works because the rules for type operations (including the new one $\to$) are defined to mirror those of categorical universal properties.
\end{proof}

\begin{rmk}\label{rmk:ctx-judgment}
  Throughout this chapter, we have been taking the notion of ``finite list'' as given externally: the context of a judgment is a finite list of types, and we assume we know what a finite list means.
  However, it is also possible to incorporate the definition of ``finite list'' into the type theory, by adding a \emph{judgment for contexts} alongside the judgment for types.
  The rules for this judgment are:
  \begin{mathpar}
    \inferrule{ }{\types () \ctx}\and
    \inferrule{\types \Gamma \ctx \\ \types A \type}{\types (\Gamma,A)\ctx}
  \end{mathpar}
  In other words, there is an empty context, and from any context we can make a new one by adding a type on the end.

  We then have the problem of expressing the other rules that modify the context in terms of this judgment.
  This is simplest and most useful in the cartesian case, when all the structural context rules (exchange, contraction, weakening) are admissible as in this section.
  For in this case, all the rules that change the context (like $\toI$ and $\plusE$) simply add an extra type at the end of it when passing from the conclusion to some of the premises, and this operation is directly represented by the second rule for the context judgment.

  We also have to deal with the ``identity/variable'' rule.
  Instead of it having a condition $(x:A)\in \Gamma$ (relying on our external knowledge of what it means to ``be an element of a finite list''), we can introduce another new judgment ``$\Gamma \types x\var A$'' meaning ``$x$ is a variable of type $A$ in context $\Gamma$'', with rules
  \begin{mathpar}
    \inferrule{\types \Gamma \ctx \\ \types A \type}{\Gamma,A \types \pop\var A}\and
    \inferrule{\types \Gamma \ctx \\ \types A \type \\ \Gamma \types x\var B}{\Gamma,A \types \shf(x)\var B}\and
    \inferrule{\Gamma \types x\var A}{\Gamma\types \use(x):A}.
  \end{mathpar}
  That is, there is a variable associated to the last type in a context, and variables associated to other types in the context are defined inductively.
  Thus, for example, the variables in the context $A,B,C$ are
  \begin{mathpar}
    \inferrule*{ }{A,B,C \types \pop\var C}\and
    \inferrule*{\inferrule*{ }{A,B \types \pop\var B}}{A,B,C\types \shf(\pop)\var B}\and
    \inferrule*{\inferrule*{\inferrule*{ }{A \types \pop\var A}}{A,B\types \shf(\pop)\var A}}{A,B,C\types \shf(\shf(\pop))\var A}\and
  \end{mathpar}
  Note that modulo a change of notation, these ``variables'' are precisely \emph{de Bruijn indices}: the number of ``$\shf$''s says how many types we need to ``count backwards'' from the right.
  At present this is merely a curiosity, but when we come to consider dependent type theories in \cref{chap:dtt} it will be much more important.
\end{rmk}


\subsection*{Exercises}

\begin{ex}\label{ex:stlc-cartmulti}
  Complete the proof in \cref{thm:stlc-initial} that type theory yields a cartesian multicategory by checking \cref{defn:fS-multicategory}\ref{item:cartmulti-3} and \ref{item:cartmulti-4}, or perhaps the corresponding one-place axioms you found in \cref{ex:cartmulti-oneplace}.
\end{ex}

\begin{ex}\label{ex:church-numerals}\ 
  \begin{enumerate}
  \item For any natural number $n$ and any type $A$ in STLC, show that there is a term of type $(A\to A)\to (A\to A)$ that iterates a function $n$ types.
    Call this term $[n]_A$.
  \item Define $[n+m]_A$ in terms of $[n]_A$ and $[m]_A$.
  \item Now define $[nm]_A$ in terms of $[n]_A$ and $[m]_A$ (you may have to use $[n]_A$ or $[m]_A$ for more than one value of $A$).
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:combinatory-logic}\ 
  % TODO: Put this, Hilbert systems, and the kinds of closed categories (or at least closed posets) in the text.
  \begin{enumerate}
  \item Write down terms in the simply typed $\lambda$-calculus (with $\to$ the only type constructor) that have the following types (for arbitrary $A,B,C$):
    \begin{mathpar}
      A\to A\\
      A\to B\to A\\
      (A\to B\to C)\to (A\to B) \to (A\to C)
    \end{mathpar}
    \textit{(Remember that the type operator $\to$ associates to the right: $X\to Y\to Z$ means $X\to (Y\to Z)$.)}\label{item:cl1}
  \item By \textbf{combinatory logic} we will mean the type theory obtained from simply typed $\lambda$-calculus by \emph{removing} the $\lambda$-abstraction rule:
    \[ \xcancel{\inferrule*{\Gamma,x:A \types M:B}{\Gamma \types \lambda x.M:A\to B}} \]
    and instead adding axioms called $I$, $K$, and $S$ having the above types (for any $A,B,C$):
    \begin{mathpar}
      \inferrule{\types A\type}{\Gamma\types I_A:A\to A}\and
      \inferrule{\types A\type\\\types B\type}{\Gamma\types K_{AB}:A\to B\to A}\and
      \inferrule{\types A\type\\\types B\type\\\types C\type}{\Gamma\types S_{ABC}:(A\to B\to C)\to (A\to B) \to (A\to C)}
    \end{mathpar}
    Prove that the removed $\lambda$-abstraction rule is \emph{admissible} in \textbf{CL}.
    That is, given a derivation in combinatory logic of $\Gamma,x:A \types M:B$, we can construct a derivation in combinatory logic of $\Gamma\types [x]M:A\to B$ for some $[x]M$ (note that this is an \emph{operation} on combinatory logic terms, like substitution).\label{item:cl2}
  \item Write down some $\equiv$-laws satisfied by the $I$, $K$, and $S$ you defined in~\ref{item:cl1}, and show that when they are used as generators for an $\equiv$ for combinatory logic, it also presents a free closed cartesian multicategory.
    One way to do this is by a direct induction on derivations; another way is exhibit a bijection between its terms and those of the simply typed $\lambda$-calculus.
  \item Compare to \cref{ex:hilbert}.
  \end{enumerate}
\end{ex}


\section{Cartesian presentations}
\label{sec:cartesian-presentations}

In \cref{sec:unary-theories} we mentioned that every kind of type theory can be generalized to use an appropriate kind of ``presentation'' (or ``theory'') as input, with the main technical issue being an appropriate notion of ``1-skeleton'' for the categorical structure in question.
We have postponed dealing with 1-skeleta in this chapter until now, because they are substantially simpler in the cartesian case; but now we are ready.

As in the unary case, our goal is to build a tower of adjunctions relating ``$k$-skeletal $(\times,+,\to)$-presentations'' with ``$k$-skeleta for cartesian closed categories with coproducts'' (and similarly when some of the type operations are omitted).
For instance, a \textbf{2-skeletal $(\times,+,\to)$-presentation} consists of:
\begin{enumerate}
\item A set $\cP_0$ of objects;
\item A set $\cP_1$ of morphisms, each of which has a list of types as domain and a single type as codomain, where the ``types'' are generated from $\cP_0$ using the rules for the judgment $\types A\type$ in \cref{sec:stlc}.
  For example, such a generating morphism might have domain $(A\to B, B\times B\to A)$ and codomain $(A\to C)\times B$.
\item A set $\cP_2$ of equalities or axioms, each of which is a pair of terms generated from $\cP_1$ and the rules for the term judgment, with the same context and the same consequent.
\end{enumerate}

Unsurprisingly, the main subtlety is in the definition of 1-skeleta for cartesian multicategories, which will require us to introduce a notion of ``presheaf on a multicategory''.
However, before we dive into that, there is a simple but still very important case we can deal with first.


\subsection{Finite-product theories}
\label{sec:fp-theories}

Suppose we start from the type theory of \cref{sec:stlc} but with \emph{no} type operations --- that is, the type theory for plain cartesian multicategories.
Then just as in \cref{sec:category-presentations}, the 1-skeleta for categories coincide with the categories themselves; the new thing relative to \cref{sec:stlc} is that we allow arbitrary generating \emph{equalities} in our 2-skeletal presentations.
These presentations are generally called \textbf{finite-product theories} or \textbf{finitary algebraic theories}.

Note that because we have morphisms in our generating multigraph with arbitrary domains, we can still express ``operations'' of arbitrary finite arity even a ``product type'' operation.
Thus, finite-product theories solve the problem that we had with our \emph{unary} finite-product theories in \cref{sec:unary-theories} (which there we mostly called ``$\times$-presentations'') of having to ``pack and unpack'' terms into ordered pairs in order to apply generators to them (such as the multiplication of a monoid object).

For instance, the finite-product theory for a monoid has:
\begin{itemize}
\item One base type $A$;
\item Two generating morphisms $m\in\cG_1(A,A;A)$ and $e\in \cG_1(();A)$; and
\item The following axioms:
  \begin{mathpar}
    x:A,y:A,z:A \types m(x,m(y,z)) \equiv m(m(x,y),z) : A\and
    x:A \types m(x,e) \equiv x :A\and
    y:A \types m(e,y) \equiv y :A
  \end{mathpar}
\end{itemize}
(As is common, since $e$ is a 0-ary generator, we write just ``$e$'' instead of explicitly giving it 0 arguments like ``$e()$''.)
In this formulation, the equational proof of uniqueness of inverses from \cref{sec:intro} finally makes sense as written.
To be precise, we assume additional generators $i,j\in \cG_1(A,A)$ and axioms
\begin{mathpar}
  x:A \types m(x,i(x))\equiv e :A \and
  x:A \types m(x,j(x))\equiv e :A \and
  x:A \types m(i(x),x)\equiv e :A \and
  x:A \types m(j(x),x)\equiv e :A.
\end{mathpar}
If we write $m(x,y)$ infix as $x\cdot y$, then we can perform the computation exactly as written:
\[ x:A \types i(x) \equiv i(x) \cdot e \equiv i(x) \cdot (x \cdot j(x)) \equiv (i(x)\cdot x)\cdot j(x) \equiv e\cdot j(x) \equiv j(x) : A.\]

For emphasis, we remind the reader how this type-theoretic proof yields a conclusion about arbitrary monoid objects in arbitrary categories with products.
Given a category with products \cM, we first regard it as a cartesian multicategory.
Then the structure of a monoid object $A$ corresponds to morphisms $(A,A)\to A$ and $()\to A$ in this cartesian multicategory, satisfying the appropriate axioms, and similarly for inverse operators.

Now if \cG is the above finite-product theory, it generates the free cartesian multicategory $\F\bCartMulti\cG$ containing a monoid object with two inverse operators.
Its freeness implies there is a unique functor of cartesian multicategories $\F\bCartMulti\cG\to \cM$ taking the generating syntactic monoid to the given one in \cM, and also its inverse operators.
Finally, the above calculation shows that $i$ and $j$ define equal morphisms in $\F\bCartMulti\cG$; hence their images in \cM must also be equal.

In general, finite-product theories can describe algebraic structures with operations and equational axioms, such as monoids, groups, rings, modules, and so on.
Thus, all such structures can be ``internalized'' in any category with finite products, and anything provable from their purely equational theory must be true in any such internalization (see for instance \cref{ex:catprod-ehnr-again}).

Finite-product theories cannot describe structures whose operations or axioms involve conditions, such as categories (we can only compose two morphisms if the source of one must equal the target of the other) or fields (we can only invert an element if it is nonzero), or whose axioms involve more complicated logical operations such as ``or'' or ``there exists''.
Structures of this sort can also be internalized, but only in a category with more structure; we will return to them in \cref{chap:fol}.

Note that we actually obtained a more general result about monoid objects in cartesian multicategories, not just categories with products, because our free object $\F\bCartMulti\cG$ is a cartesian multicategory rather than a category with products.
However, for some purposes, we might also want to have a free category with products generated by a finite-product theory.
Once we have established the full theory of presentations in \cref{sec:multicat-pshf}, we can obtain this by simply adding the $\times,\unit$ type operations.
But there is also another way to obtain a free category with products, by applying the following left adjoint (which, for later use, we construct in the case of a general \fS).

\begin{thm}\label{thm:free-Smoncat-Smulti}
  Let $\bStrMonCat_\fS$ denote the category of strict \fS-monoidal categories; that is, \fS-multicategories that are representable and whose underlying monoidal category is strict, and functors that preserve the chosen tensor products strictly.
  The forgetful functor from $\bStrMonCat_\fS$ to \fS-multicategories has a left adjoint $\cM\mapsto\catctx\cM$.
\end{thm}
\begin{proof}
  Given an \fS-multicategory \cM, we define the objects of $\catctx\cM$ to be finite lists $(A_1,\dots,A_n)$ of objects of \cM, with a monoidal structure given by concatenation of lists.
  The hom-set $\catctx\cM((A_1,\dots,A_n),(B_1,\dots,B_k))$ is a subquotient (i.e.\ a quotient of a subset) of the set
  \[ \setof{(\sigma,(f_1,\dots,f_k)) | \cod(f_j) = B_j \text{ and } \sigma : \{1,\dots,m\} \to \{1,\dots,n\}\text{ in }\fS }. \]
  The subset consists of those tuples such that if we concatenate the domains of the $f_j$'s in order, we get $(A_{\sigma 1},\dots, A_{\sigma m})$.
  The quotient is then
  % \begin{equation*}
  %   \coprod_{(0 = i_0 \le i_1 \le \cdots \le i_{k-1} \le i_k = m)}\;
  %   \coprod_{(\sigma : \{1,\dots,m\} \to \{1,\dots,n\}\text{ in }\fS)}\;
  %   \prod_{j=1}^{k} \cM(A_{\sigma(i_{j-1}+1)},\dots,A_{\sigma (i_{j})}; B_j)
  % \end{equation*}
  by the smallest equivalence relation that identifies
  \[ (\sigma, (f_1 \sigma_1^* ,\dots, f_k \sigma_k^*))
  \qquad\text{with}\qquad
  (\sigma(\sigma_1\sqcup \cdots \sqcup \sigma_k),(f_1,\dots,f_k))\]
  (This can be described more abstractly as a ``tensor product of functors''.)
  % The identity morphism of $(A_1,\dots,A_n)$ is (the equivalence class of) $(\idfunc_n,(\idfunc_{A_1},\dots,\idfunc_{A_n}))$.
  Composition is defined on representatives by
  \begin{multline*}
    (\tau,(g_1,\dots,g_n)) \circ (\sigma,(f_1,\dots,f_k)) =\\
    (\tau(\sigma\wr \ell_1,\dots,\ell_n), (g_{\sigma 1},\dots,g_{\sigma m})\circ (f_1,\dots,f_k))
  \end{multline*}
  Here $\ell_j$ is the arity of $g_j$, and $(g_{\sigma 1},\dots,g_{\sigma m})\circ (f_1,\dots,f_k)$ means to compose the first few $g_{\sigma i}$'s with $f_1$ (according to the arity of $f_1$), then the next few with $f_2$, and so on.
  We leave the details to the reader.

  There are two cases in which $\catctx\cM$ has a simpler description.
  Firstly, if \fS contains only identities, so we are talking about ordinary multicategories and monoidal categories, then the coproduct over $\sigma$ degenerates and there is no quotienting necessary; so the above definition is complete.
  Secondly, in the cartesian case when \fS contains all functions, we can instead define
  \[\catctx\cM((A_1,\dots,A_n),(B_1,\dots,B_k)) =
  \prod_{j=1}^k \cM(A_1,\dots,A_n; B_j).
  \]
  To see that this definition is isomorphic to the previous one in the cartesian case, note that since $(B_1,\dots,B_k)$ is the cartesian product $B_1\times \cdots \times B_k$ in $\catctx\cM$, we must have
  \[\catctx\cM((A_1,\dots,A_n),(B_1,\dots,B_k)) =
  \prod_{j=1}^k \catctx\cM((A_1,\dots,A_n); B_j).
  \]
  Thus, it suffices to observe that $\catctx\cM((A_1,\dots,A_n); B) \cong \cM(A_1,\dots,A_n; B)$.
  This is because when $k=1$, the quotient precisely cancels out the extra $\sigma$ involved in the former.
\end{proof}

If we apply this left adjoint to the free cartesian multicategory generated by a finite-product theory \cP, we obtain a category with products whose objects are the \emph{contexts} in the type theory of \cP, and whose morphisms are tuples of terms.
For this reason it is often called the \textbf{category of contexts} of \cP.

When \cP has exactly one type, say $A$, the objects of its category of contexts are just lists $(A,A,\dots,A)$ uniquely determined by their length, and so they can be identified with natural numbers.
In this case, the category of contexts is known as the \textbf{Lawvere theory}~\cite{lawvere:functsem} corresponding to \cP (recall from \cref{sec:theories} that some categorical logicians use the word ``theory'' to refer to the categorical structure \emph{presented by} a type theory).

Of course, the universal property of the category of contexts given by \cref{thm:free-Smoncat-Smulti} refers only to \emph{strict} monoidal categories, which makes sense since concatenation of contexts is strictly associative.
However, it turns out that up to equivalence, it also has a more general universal property.

\begin{thm}\label{thm:free-catprod-cartmulti}
  Let $\sPrCat$ denote the 2-category of categories with products, functors that preserve products up to isomorphism in the usual sense, and natural transformations; and let \sCartMulti denote the 2-category of cartesian multicategories.
  The forgetful functor $\sPrCat\to\sCartMulti$ has a left adjoint constructed exactly as in \cref{thm:free-Smoncat-Smulti}.
\end{thm}
\begin{proof}
  This can be proven directly and concretely (see \cref{ex:free-catprod-cartmulti}); but it also follows from general theory of 2-monads~\cite{bkp:2dmonads} and the fact that categories with products are 2-monadic over cartesian multicategories.
\end{proof}

Thus, up to equivalence, the category of contexts of a finite-product theory \cP is the free category-with-products generated by \cP.
In particular, it uniquely determines, up to equivalence, the category of morphisms of theories from \cP into any category with products (such morphisms are often called \textbf{models} of the theory): they are the same as product-preserving functors out of the category of contexts.
This example was the original observation of Lawvere~\cite{lawvere:functsem} that gave rise to categorical logic.

Intuitively, the category of contexts can be said to contain the ``extensional essence'' of a finite-product theory.
As mentioned in \cref{sec:theories}, two theories that generate equivalent categories of contexts have ``the same models'' in all categories, and are said to be \textbf{Morita equivalent}.
For instance, the notion of group can be presented with a multiplication, unit, and inverse, or with a unit and ``division'' operation; these are distinct theories but are Morita equivalent.
(The study of finite-product theories, particularly those with only one type, is also known as \emph{universal algebra}; although classical universal algebraists mainly study models in \bSet rather than more general categories.)

\begin{rmk}
  This seems an appropriate place to mention an alternative approach to terms in type theory that is fairly common, especially for finite-product theories.
  Rather than giving rules that inductively generate judgments (with contexts) and then assigning terms to represent them uniquely with variables associated to the types in the context, some authors instead suppose given from the start a different collection of ``variables'' associated to each type.
  Then the terms (without contexts) are defined inductively by applying generating morphisms to variables of appropriate types, and finally a ``valid context for a term'' is \emph{defined} to be any list of variables (with their associated types) that includes all the variables appearing (freely) in the term.
  The end result is much the same, but our way of keeping track of the context all the way through matches the category theory better (since every morphism in a category has a specified domain) and makes for cleaner inductive arguments.
\end{rmk}


\subsection{Presheaves on multicategories}
\label{sec:multicat-pshf}

Now we move on to cartesian theories with type operations, and hence 1-skeleta that differ from the 2-skeleta.
This will require us to discuss ``contravariant representable functors'' for a multicategory; but what are those?
More specifically, what \emph{sort of thing} are they?
Inspecting the structure possessed by the family of sets $\cM(A_1,\dots,A_n;B)$, for a fixed $B$ as the $A_i$ vary, leads us to the following definition.

\begin{defn}\label{defn:multicat-pshf}
  Let \cM be an \fS-multicategory and \bC a category.
  A \textbf{\bC-valued presheaf on \cM} consists of
  \begin{enumerate}
  \item For each list $(A_1,\dots,A_n)$ of objects of \cM, an object $\cH(A_1,\dots,A_n)\in\bC$.
  \item For each list $(f_1,\dots,f_m)$ of morphisms of \cM, with $f_i:(A_{i1},\dots,A_{in_i})\to B_i$, a morphism in \bC:
    \[ (f_1,\dots,f_n)^* : \cH(B_1,\dots,B_m) \to \cH(A_{11},\dots,A_{mn_m}) \]
    which are associative and unital with respect to composition in \cM:
    \begin{align*}
      (f_{11},\dots,f_{mn_m})^* \circ (g_1,\dots,g_m)^* &=
      (g_1\circ (f_{11},\dots,f_{1n_1}), \dots, g_m \circ (f_{m1},\dots,f_{mn_m}))^*
      \\
      (\idfunc_{A_1},\dots,\idfunc_{A_n})^* &= \idfunc_{\cH(A_1,\dots,A_n)}
    \end{align*}
  \item For each $\sigma : \{1,\dots,m\} \to \{1,\dots,n\}$ in \fS, a morphism in \bC:
    \[ \sigma^* : \cH(A_{\sigma 1},\dots,A_{\sigma m}) \to \cH(A_1,\dots,A_n) \]
    such that
    \begin{align*}
      (f_1 \sigma_1^* ,\dots, f_n \sigma_n^*)^* &=
      (\sigma_1\sqcup \cdots \sqcup \sigma_n)^*\circ (f_1,\dots,f_n)^*\\
      (f_1,\dots,f_n)^* \circ \sigma^* &=
      (\sigma \wr (k_1,\dots,k_n))^*\circ(f_{\sigma 1},\dots, f_{\sigma m})^*
    \end{align*}
    where $k_i$ is the arity of $f_i$.
  \end{enumerate}
\end{defn}

Conveniently, it turns out that this definition can be reformulated as an ordinary functor on a different category:

\begin{thm}\label{thm:multicat-pshf-catctx}
  For any \fS-multicategory \cM, a \bC-valued presheaf on \cM as in \cref{defn:multicat-pshf} is the same as an ordinary functor $\catctx\cM\op \to \bC$, where $\catctx\cM$ is as in \cref{thm:free-Smoncat-Smulti}.
\end{thm}
\begin{proof}
  A functor $\cH:\catctx\cM\op \to \bC$ certainly associates an object of \bC to each list $(A_1,\dots,A_n)$ of objects of \cM.
  The action of a morphism $(\sigma,(f_1,\dots,f_k))$ in $\catctx\cM$ corresponds to the composite $\sigma^*\circ (f_1,\dots,f_k)^*$ of a \bC-valued presheaf, and the latter actions can be recovered from it by putting in identities for $\sigma$ or the $f$'s.
  The axiom of a \bC-valued presheaf involving $\sigma_1\sqcup\cdots\sqcup\sigma_n$ comes from the quotient involved in the hom-sets of $\catctx\cM$, while the other axioms come from the definition of identities and composition in $\catctx\cM$.
\end{proof}

For instance, this immediately implies a Yoneda lemma:

\begin{cor}\label{thm:multicat-yoneda}
  For any \fS-multicategory \cM, object $B\in\cM$, and \bSet-valued presheaf \cH on \cM, there is a natural bijection between natural transformations $\cM(-;B) \to \cH$ and elements of $\cH(B)$.\qed
\end{cor}

Specializing all of this to the cartesian case, we can now define a \textbf{1-skeleton for a cartesian closed category with coproducts}.
It consists of the following (compare to the rules in \cref{fig:stlc}):
\begin{enumerate}
\item A set $\cM_0$ of objects with chosen elements $\unit,\zero$ and binary operations $\times,+,\to$.
\item A cartesian multicategory $\cM$ with $\cM_0$ as set of objects.
\item For each $A,B\in\cM_0$, morphisms $A\times B\to A$ and $A\times B\to B$ and a natural transformation of \bSet-valued presheaves on \cM:
  \[ \cM(-;A) \times \cM(-;B)\too \cM(-;A\times B) \]
\item A natural transformation of \bSet-valued presheaves $1\to \cM(-;\unit)$.
\item For each $C\in\cM_0$, a morphism $\zero\to C$.
\item For each $A,B\in\cM_0$, morphisms $A\to A+B$ and $B\to A+B$; and for any $A,B,C$ a natural transformation:
  \[ \cM(-;A+B) \times \cM(-,A;C) \times \cM(-,B;C) \too \cM(-;C) \]
\item For any $A,B\in \cM_0$, natural transformations:
  \[ \cM(-,A;B) \too \cM(-;A\to B) \]
  \[ \cM(-;A\to B) \times \cM(-;A) \too \cM(-;B). \]
\end{enumerate}
With this we can construct a tower of adjunctions as in \cref{sec:unary-theories}:
\[ \xymatrix{
  \stlcpres 2 \ar@<2mm>[r]^-{\F{2}} \ar@{}[r]|-{\bot} \ar[d] & \cccc 2 \ar@<2mm>[l]^-{\fU_2} \ar[d] \\
  \stlcpres 1 \ar@<2mm>[r]^-{\F{1}} \ar@{}[r]|-{\bot} \ar[d] & \cccc 1 \ar@<2mm>[l]^-{\fU_1} \ar[d] \\
  \stlcpres 0 \ar@<2mm>[r]^-{\F{0}} \ar@{}[r]|-{\bot}        & \cccc 0 \ar@<2mm>[l]^-{\fU_0}
}\]
where $\stlcpres k$ denotes the category of $k$-skeletal $(\times,+,\to)$-presentations, and $\cccc k$ denotes the category of $k$-skeleta for cartesian closed categories with coproducts.
(The 1-skeleta were defined above, the 2-skeleta are simply the categories themselves, and the 0-skeleta are sets equipped with operations $\times,+,\to$ and elements $\unit,\zero$.)

We can also omit any of the type operations, by the modularity of type theory (principle~\eqref{princ:independence}).
And we can show as in \cref{sec:unary-theories} that every category of the appropriate sort is presented by its underlying presentation (or ``internal logic''); so that if we define the morphisms between presentations appropriately we obtain an equivalence of bicategories.
In particular, $(\times,\to)$-presentations (which are often given a name like ``$\lambda_\times$-theories'') can be assembled into a bicategory that is equivalent to that of cartesian closed categories.
The discovery by Lambek~\cite{lambek:stlc-ccc} of this relationship between simply typed $\lambda$-calculus and cartesian closed categories was another important milestone in the development of categorical logic.


\subsection*{Exercises}

\begin{ex}\label{ex:catprod-ehnr-again}
  Re-do \cref{ex:catprod-eckmann-hilton,ex:catprod-nearring} using finite-product theories.
  Notice how much nicer they are.
\end{ex}

\begin{ex}\label{ex:catprod-thy-noprod}
  Let $\cG$ be a (non-unary) $\times,\unit$-theory, i.e.\ a multicategorical theory whose only type operations are $\times,\unit$, but whose generating morphisms can involve $\times,\unit$ in their domains and codomains, and with generating equalities.
  Show that there is another $\times$-theory \cH whose generating arrows contain only base types in their domains and codomains and such that $\F\bPrCat\cG\simeq \F\bPrCat\cH$.
\end{ex}

\begin{ex}\label{ex:free-Smoncat-Smulti}
  Complete the proof of \cref{thm:free-Smoncat-Smulti} by showing that the claimed definition does in fact define a left adjoint.
  Also verify the claimed simpler description of the hom-sets in the cartesian case.
\end{ex}

\begin{ex}\label{ex:free-catprod-cartmulti}
  Prove \cref{thm:free-catprod-cartmulti}.
\end{ex}

\begin{ex}\label{ex:catctx-ctxjdg}
  By using induction over the ``context judgment'' from \cref{rmk:ctx-judgment}, prove directly that the category of contexts of a finite-product theory has a universal property up to equivalence among categories with products.
\end{ex}

% \section{Programming with $\lambda$-calculus}
% \label{sec:primrec}

% [NNOs, primitive recursion, functional programming, perhaps more general GADTs]


\section{Symmetric monoidal categories}
\label{sec:symmoncat}

Now we consider a type theory for symmetric monoidal categories.
That is, we add the exchange rule (and the $\hom$ rules) to \cref{sec:multicat-prod-coprod}, or remove weakening and contraction from \cref{sec:stlc}.

\subsection{Shuffles}
\label{sec:shuffles}

As always for structural rules, we want exchange to be admissible.
But we cannot use the same trick for this that we did in \cref{sec:stlc}, because in the absence of weakening the identity rule must be $x:A\types x:A$ rather than containing a whole context on the left.
Thus, we cannot expect to push exchange all the way up to the top; instead we need to build it into the other rules.
For instance, in the theory of \cref{sec:logic} we can derive $B,A\types A\tensor B$ by using primitive exchange:
\[ \inferrule*{\inferrule*{A\types A \\ B\types B}{A,B\types A\tensor B}}{B,A\types A\tensor B} \]
To obtain this without primitive exchange, we must incorporate some exchange into the $\tensorI$ rule.
That is, it must say something like
\[ \inferrule{\Gamma\types A \\ \Delta\types B \\ \Gamma,\Delta \cong \Phi}{\Phi\types A\tensor B} \]
allowing us to permute the concatenated context $\Gamma,\Delta$ of the premises to obtain the context of the conclusion.

However, this is not quite right yet: it introduces too much redundancy.
For instance, with this rule we would have the following derivation of $A,B,C\types A\tensor (B\tensor C)$:
\begin{mathpar}
  \inferrule*{A\types B \\ \inferrule*{B\types B \\ C\types C \\ B,C\cong C,B}{C,B\types B\tensor C} \\ A,C,B\cong A,B,C}{A,B,C\types A\tensor (B\tensor C)}
\end{mathpar}
which would be distinct from the obvious one:
\begin{mathpar}
  \inferrule*{A\types B \\ \inferrule*{B\types B \\ C\types C \\ B,C\cong B,C}{B,C\types B\tensor C} \\ A,B,C\cong A,B,C}{A,B,C\types A\tensor (B\tensor C)}
\end{mathpar}
This is not what we want; both clearly represent the same morphism in a symmetric multicategory, and moreover both are naturally represented by the same term $x:A,y:B,z:C \types \tpair{x}{\tpair{y}{z}}:A\tensor (B\tensor C)$.
What we need to do is incorporate ``just enough'' exchange to obtain any desired ordering of the context of the conclusion, but without introducing redundancy.

The redundancy comes from the fact that the contexts of the premises must already be free to occur in any order.
Thus, we don't want to re-build-in permutations of those, only permutations that alter the relative order between the contexts of different premises.
Formally, what we need is a \emph{shuffle}.

\begin{defn}
  For $p_1,\dots,p_n \in \dN$, a \textbf{$(p_1,\dots,p_n)$-shuffle} is a permutation of $\bigsqcup_{i=1}^n\{1,\dots,p_i\}$ with the property that it leaves invariant the internal ordering of each summand.
\end{defn}

For instance, if we write $\{1,2\}\sqcup \{1,2,3\}$ as $\{1,2,1',2',3'\}$, then here are some $(2,3)$-shuffles:
\begin{mathpar}
  121'2'3'\and
  11'2'23'\and
  1'2'13'2\and
  1'12'3'2
\end{mathpar}
In all cases $1$ comes before $2$, and also $1'$ comes before $2'$ which comes before $3'$.
The name ``shuffle'', of course, comes from the fact that when $n=2$ this is exactly the sort of permutation that can be obtained by cutting a deck of $p+q$ cards into a $p$-stack and a $q$-stack and riffle-shuffling them together.

Now let $S_p$ denote the symmetric group on $p$ elements; thus the $(p_1,\dots,p_n)$-shuffles are elements of $S_{p_1+\cdots+p_n}$.
Note that they are not a subgroup.
However, we do have a (non-normal) inclusion $S_{p_1}\times \cdots\times S_{p_n} \into S_{p_1+\cdots+p_n}$ given by the \textbf{block sum of permutations}, acting on $\bigsqcup_{i=1}^n\{1,\dots,p_i\}$ by permuting each summand individually.
The following is straightforward to verify.

\begin{lem}
  Every coset of $S_{p_1}\times \cdots \times S_{p_n}$ in $S_{p_1+\cdots+p_n}$ contains exactly one $(p_1,\dots,p_n)$-shuffle.
  Thus, every permutation of $p_1+\cdots+p_n$ can be written uniquely as the product of a block sum from $S_{p_1}\times \cdots \times S_{p_n}$ and a $(p_1,\dots,p_n)$-shuffle.\qed
\end{lem}

If $\Gamma_i$ is a context of length $p_i$ for $i=1,\dots,n$, then we write $\nShuf(\Gamma_1,\dots,\Gamma_n;\Psi)$ for the set of $(p_1,\dots,p_n)$-shuffles that act on the concatenated context $\Gamma_1,\dots,\Gamma_n$ to produce the context $\Psi$.
When using named variables, we assume that the variable names are preserved by this action (which means that the contexts $\Gamma_1,\dots,\Gamma_n$ and $\Psi$ uniquely determine such a shuffle if it exists).
Now we can state a better version of $\tensorI$:
\[ \inferrule{\Gamma\types A \\ \Delta\types B \\ \sigma\in\nShuf(\Gamma,\Delta;\Phi)}{\Phi\types A\tensor B} \]
This allows deriving $B,A\types A\tensor B$, but rules out the undesired redundant derivation above, since the permutation $A,C,B\cong A,B,C$ is not a $(1,2)$-shuffle.
We can treat all the other rules from \cref{sec:multicat-prod-coprod} (and also the $\hom$ rules) similarly, moving the active types in the context to the far right as we did in \cref{sec:stlc}; the result is shown in \cref{fig:smc}.

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{\types A\type}{x:A\types x:A}\;\idfunc
    \and
    \inferrule{f\in \cG(A_1,\dots,A_n;B) \\ \Gamma_1\types M_1:A_1 \\ \dots \\ \Gamma_n \types M_n:A_n \\ \nShuf(\Gamma_1,\dots\Gamma_n;\Phi)}{\Phi\types f(M_1,\dots,M_n):B}\;fI
    \and
    \inferrule{\Gamma\types M:A \\ \Delta\types N:B \\ \nShuf(\Gamma,\Delta;\Phi)}{\Phi\types \tpair{M}{N}:A\tensor B}\;\tensorI
    \and
    \inferrule{
      \Psi \types M:A\tensor B \\
      \Gamma,x:A,y:B\types N:C\\
      \nShuf(\Gamma,\Psi;\Phi)
    }{
      \Phi \types \match_{A\tensor B}(M,xy.N):C
    }\;\tensorE
    \\
    \inferrule{ }{\ec\types \ott:\one}\;\one I
    \and
    \inferrule{
      \Psi\types M:\one \\
      \Gamma\types N:C \\
      \nShuf(\Gamma,\Psi;\Phi)
    }{
      \Phi\types \match_\one(M,N):C
    }\;\one E
    \\
    \inferrule{\Gamma\types M:A \\ \Gamma\types N:B}{\Gamma\types \pair{M}{N} :A\times B}\;\timesI
    \and
    \inferrule{\Gamma\types M:A\times B}{\Gamma\types \pr1AB(M):A}\;\timesE1
    \and
    \inferrule{\Gamma\types M:A\times B}{\Gamma\types \pr2AB(M):B}\;\timesE2
    \\
    \inferrule{ }{x_1:A_1,\dots,x_n:A_n\types \ttt(x_1,\dots,x_n):\unit}\;\unit I
    \and
    \inferrule{\Psi\types M:\zero \\ \nShuf(\Gamma,\Psi;\Phi)}{\Phi\types \abort^\Gamma(M):C}\;\zero E
    \\
    \inferrule{\Gamma\types M:A}{\Gamma\types \inl(M):A+B}\;\plusI1
    \and
    \inferrule{\Gamma\types N:B}{\Gamma\types \inr(N):A+B}\;\plusI2
    \and
    \inferrule{
      \Psi\types M:A+B \\ \Gamma,u:A \types P:C \\ \Gamma,v:B\types Q:C \\ \nShuf(\Gamma,\Psi;\Phi)
    }{\Phi \types\acase AB(M,u.P,v.Q):C}\;\plusE\and
    \inferrule{\Gamma,x:A\types M:B}{\Gamma\types \lambda x.M:A\hom B}\;\homI\and
    \inferrule{\Gamma\types M:A\hom B \\ \Delta\types N:A \\ \nShuf(\Gamma,\Delta;\Phi)}{\Phi\types M N:B}\;\homE
  \end{mathpar}
  \caption{Type theory for symmetric monoidal categories}
  \label{fig:smc}
\end{figure}

\begin{lem}\label{thm:smc-exchadm}
  Exchange is admissible in this type theory: if we have a derivation of $\Gamma\types A$, and a permutation $\Gamma\cong \Delta$ rearranging $\Gamma$ to $\Delta$, then we can construct a derivation of $\Delta\types A$.
  Moreover, this operation is a group action.
\end{lem}
\begin{proof}
  We induct on the given derivation of $\Gamma\types A$, and most of the cases are essentially the same.
  Consider $\tensorI$: given its premises and a permutation $\Phi\cong\Phi'$, we decompose the composite permutation $\Gamma,\Delta\cong \Phi\cong\Phi'$ uniquely as the block sum of two permutations $\Gamma\cong \Gamma'$ and $\Delta\cong\Delta'$ with a shuffle $\Gamma',\Delta' \cong \Phi'$.
  Now by the inductive hypothesis we can derive $\Gamma'\types A$ and $\Delta'\types B$, whence applying $\tensorI$ again with the shuffle $(\Gamma',\Delta') \cong \Phi'$ we get $\Phi' \types A\tensor B$.
  All the other cases can be treated similarly.

  We likewise show that it is a group action by induction.
  In the case of $\tensorI$, if we have $\Phi\cong \Phi'\cong\Phi''$, we decompose $(\Gamma,\Delta)\cong \Phi\cong \Phi'$ as $(\Gamma,\Delta)\cong (\Gamma',\Delta')\cong\Phi'$; then we decompose $(\Gamma',\Delta')\cong\Phi' \cong \Phi''$ as $(\Gamma',\Delta')\cong (\Gamma'',\Delta'')\cong\Phi''$.
  But since composition of permutations is associative, this is the same as decomposing $(\Gamma,\Delta)\cong \Phi\cong \Phi''$ as $(\Gamma,\Delta)\cong (\Gamma'',\Delta'')\cong \Phi''$ directly.
  We conclude by applying the inductive hypothesis to the actions of $\Gamma\cong \Gamma'\cong \Gamma''$ and $\Delta\cong \Delta'\cong\Delta''$ on the premises.
\end{proof}

Note that the shuffles appearing in the premises are \emph{not} notated explicitly in the terms!
Nevertheless, terms still uniquely determine derivations, because we can inspect the order that the variables appear in a term.
As in \cref{sec:multicat-prod-coprod} we need ``superlinearity'' first.

\begin{lem}\label{thm:smc-superlin}
  If $\Gamma\types M:A$ is derivable, then every variable in $\Gamma$ appears at least once (free) in $M$.
\end{lem}
\begin{proof}
  An easy induction just like \cref{thm:moncat-prod-coprod-superlin}.
  Note that we again had to include the unused variables in $\unit I$ and $\zero E$ for this purpose.
\end{proof}

\begin{lem}\label{thm:smc-tad}
  If $\Gamma\types M:A$ is derivable, then it has a unique derivation.
\end{lem}
\begin{proof}
  By induction on derivations.
  Clearly the structure of a term determines the \emph{rule} that must have been applied to produce it, so the question is whether it determines the premises uniquely as well.
  The interesting cases are the rules that involve shuffles: $fI,\tensorI,\tensorE,\one E,\zero E,\plusE$.

  Consider $\tensorI$: looking at the conclusion $\Phi \types \tpair M N : A \tensor B$, the rule ensures that each variable in $\Phi$ can only occur in one of $M$ or $N$, and by \cref{thm:smc-superlin} it must appear in exactly one of them.
  Thus, it must be that $\Gamma$ consists of those variables occurring in $M$ while $\Delta$ consists of those variables occurring in $N$.
  Moreover, since the shuffle $\nShuf(\Gamma,\Delta;\Psi)$ cannot alter the relative order of variables in $\Gamma$ and $\Delta$, it must be that the variables in $\Gamma$ and $\Delta$ occur in the same order as they do in $\Psi$.
  Thus the premises $\Gamma\types M:A$ and $\Delta\types N:B$ are uniquly determined, and once $\Gamma$ and $\Delta$ are fixed the shuffle is also uniquely determined.
  All the other rules involving shuffles behave similarly.
\end{proof}

From this point onwards the theory looks almost exactly like that of \cref{sec:multicat-prod-coprod}: substitution is admissible, we define $\beta$- and $\eta$-conversion rules, and construct a free closed symmetric monoidal category with products and coproducts (or less, by omitting some of our type operations).
We leave the details to the reader (\cref{ex:smc}).

In particular, because we have ensured that terms uniquely represent derivations, we can prove the initiality theorem as usual by a simple induction over derivations.
To the author's knowledge the use of shuffles for this purpose is an improvement over the existing literature: it produces a free symmetric multicategory using nice-looking terms while still maintaining the ``terms are derivations'' principle, so that we can prove the initiality theorem without incurring the (rarely-satisfied) obligation to prove that definitions by induction over derivations depend only on the term.

One sometimes also finds remarks that the context in a linear type theory can be treated as a ``finite multiset'' (a ``set that can contain some elements more than once'').
Whether this is true depends on what exactly one means by a multiset.
On one hand, if a multiset just means a set with a (finite) positive ``count'' labeling each element, then this is true for posetal linear logic as in \cref{sec:logic}, but not when we want to present non-posetal symmetric monoidal categories, since it doesn't allow us to distinguish between $x:A,y:A \types \tpair x y:A\tensor A$ and $x:A,y:A \types \tpair y x:A\tensor A$.
On the other hand, if a multiset means a set with a (finite) nonempty \emph{set} of ``occurrences'' labeling each element, then the occurrences play essentially the same role as named variables.
This suggests a type theory corresponding somehow to the ``fat symmetric multicategories'' of~\cite[Appendix A]{leinster:higher-opds}; but we will not pursue this further.


\subsection{Symmetric $\tensor$-presentations}
\label{sec:symm-tensor-pres}

We can now enhance the theory of \cref{sec:shuffles}, like in \cref{sec:unary-theories}, to take a ``presentation'' as input.
That is, we  allowing generating morphisms with arbitrary types in their domains and codomains, as well as generating equalities relating arbitrary pairs of parallel terms.

As in \cref{sec:fp-theories}, the simplest case is if we omit all type operations (so that we have a theory only of symmetric multicategories, which coincide with their 1-skeleta) but allow arbitrary generating equalities.
In this case we obtain what might be called \textbf{linear finitary algebraic theories}: a set of types, a set of operations with finite arities and types, and a set of axioms about the the composites of those operations such that ``each variable appears exactly once on both sides of each axiom''.
For instance, the theory of monoids is linear, with the axioms:
\begin{align*}
  x:A,y:A,z:A &\types x\cdot (y\cdot z) \equiv (x\cdot y)\cdot z :A\\
  x:A &\types x\cdot e \equiv x:A\\
  x:A &\types e\cdot x \equiv x:A
\end{align*}
but the theory of groups, which adds a unary operation $i$ and the axioms
\begin{align*}
  x:A &\types x\cdot i(x) \equiv e:A \\
  x:A &\types i(x)\cdot x \equiv e:A
\end{align*}
is not.
Note that formally, we do not have to give a precise meaning to ``each variable appears exactly once on both sides of each axiom''; instead the terms that can appear in axioms are defined inductively by rules that happen to \emph{ensure} that this condition holds.

If \cG is a linear finitary algebraic theory, then of course it generates a free symmetric multicategory $\F\bSymMulti\cG$ whose objects are precisely the (base) types of \cG.
In particular, if \cG has one type, then $\F\bSymMulti\cG$ has one object.
A (symmetric) multicategory with one object is called an \textbf{operad} (enriched in \bSet --- though much of the interest of operads lies in operads enriched in other categories); they were originally defined by~\cite{may:goils}, and the terminology has since been much generalized~\cite{leinster:higher-opds}.
(Indeed, arbitrary multicategories are sometimes called ``colored operads''.)

On the other hand, there are cases where we want to allow tensor products in the codomain.
For instance, the theory of bimonoids \begin{props}mentioned in \cref{sec:intro} \end{props}would have one type $A$, four generating morphisms
\begin{mathpar}
  m:(A,A)\to A\and
  e:() \to A\and
  \comult:A\to A\tensor A\and
  \counit : A\to \one
\end{mathpar}
and the axioms shown in \cref{fig:smc-bimonoid}.

\begin{figure}
  \centering
  \begin{align*}
    x:A,y:A,z:A &\types x\cdot (y\cdot z) \equiv (x\cdot y)\cdot z :A\\
    x:A &\types x\cdot e \equiv x:A\\
    x:A &\types e\cdot x \equiv x:A\\
    x:A &\types
          \begin{multlined}[t]
            \match_\tensor(\comult(x),uv.\tpair{u}{\comult(v)})\\[\jot]
            \equiv
            \match_\tensor(\comult(x),uv.\match_\tensor(\comult(u),wz.\tpair{w}{\tpair{z}{v}})\\
            : A\tensor (A\tensor A)
          \end{multlined}\\
    x:A &\types \match_\tensor(\comult(x),uv.\match_\one(\counit(u),v)) \equiv x : A\\
    x:A &\types \match_\tensor(\comult(x),uv.\match_\one(\counit(v),u)) \equiv x : A\\
    x:A,y:A &\types
              \begin{multlined}[t]
                \match_\tensor(\comult(x),uv,\match_\tensor(\comult(y),wz.\tpair{m(u,w)}{m(v,z)}))\\[\jot]
                \equiv \comult(m(x,y)) : A\tensor A
              \end{multlined}\\
    x:A,y:A &\types \counit(m(x,y)) \equiv \match_\one(\counit(x),\match_\one(\counit(y),\ott)) :\one\\
    \ec &\types \comult(e) \equiv \tpair{e}{e} :A\tensor A\\
    \ec &\types \counit(e) \equiv \ott :\one
  \end{align*}
  \caption{Axioms for a bimonoid}
  \label{fig:smc-bimonoid}
\end{figure}

To make sense of this, we need a notion of 1-skeleton that can describe the naturality properties of the type operations from \cref{fig:smc}.
This requires the notion of ``presheaf on a multicategory'' from \cref{sec:multicat-pshf} (which we intentionally defined for arbitrary \fS so that we could use it here too).
Here, however, we will need not just the category of such presheaves but a \emph{multicategory} of them.

\begin{thm}\label{thm:multicat-day}
  Let \cM and \cC be \fS-multicategories.
  Then there is an \fS-multicategory whose objects are presheaves on \cM valued in the underlying ordinary category of \cC, as in \cref{defn:multicat-pshf}.

  A morphism $(\cH_1,\dots,\cH_n)\to\cK$ (called an \textbf{$n$-ary natural transformation}) consists of
  for each $A_{11},\dots,A_{n m_n}$, a morphism in \cC:
  \[ \alpha : (\cH(A_{11},\dots,A_{1 m_1}),\dots,\cH(A_{n1},\dots,A_{n m_n})) \too \cK(A_{11},\dots,A_{n m_n}) \]
  such that
  \begin{align*}
    \alpha\circ (\sigma_1^*,\dots,\sigma_n^*) &= (\sigma_1\sqcup\cdots\sqcup\sigma_n)^*\circ\alpha\\
    \alpha\circ ((f_{11},\dots,f_{1 \ell_1})^*,\dots,(f_{k1},\dots,f_{k \ell_k})^*)
    &= (f_{11},\dots,f_{k \ell_k})^*\circ\alpha
    \thmqedhere
  \end{align*}
\end{thm}
Technically, the $\alpha$'s should have appropriate subscripts, but that would make the notation even heavier and harder to understand.

The point of this definition is to capture the behavior of substitution into a rule that concatenates two (or more) contexts in its premises (perhaps with a shuffle) to form the context of its conclusion.
With it in hand, we can define a \textbf{1-skeleton for a closed symmetric monoidal category with products and coproducts} to consist of the following (refer to \cref{fig:smc}).
\begin{enumerate}
\item A set $\cM_0$ with chosen elements $\one,\unit,\zero$ and binary operations $\tensor,\times,+,\hom$.
\item A symmetric multicategory \cM with object set $\cM_0$.
\item For each $A,B$, a 2-ary natural transformation
  \[ (\cM(-;A),\cM(-;B)) \too \cM(-;A\tensor B) \]
\item For each $A,B,C$, a 2-ary natural transformation
  \[ (\cM(-,A,B;C),\cM(-;A\tensor B)) \too \cM(-;C) \]
\item A morphism $()\to \one$.
\item For each $C$, a 2-ary natural transformation
  \[ (\cM(-;C),\cM(-;\one)) \too \cM(-;C) \]
\item For each $A,B$, morphisms $A\times B\to A$ and $A\times B\to B$ and a (1-ary) natural transformation
  \[ \cM(-;A) \times \cM(-;B) \too \cM(-;A\times B) \]
\item A natural transformation $1\to \cM(-;\unit)$.
\item For each $C\in\cM_0$, a 2-ary natural transformation
  \[ (1,\cM(-;\zero)) \too \cM(-;C) \]
  where $1$ denotes the terminal \bSet-valued presheaf on \cM.
\item For each $A,B\in\cM_0$, morphisms $A\to A+B$ and $B\to A+B$; and for any $A,B,C$ a 2-ary natural transformation:
  \[ (\cM(-,A;C) \times \cM(-,B;C) , \cM(-;A+B)) \too \cM(-;C) \]
\item For any $A,B\in \cM_0$, a natural transformation
  \[ \cM(-,A;B) \too \cM(-;A\hom B) \]
\item For any $A,B\in \cM_0$, a 2-ary natural transformation
  \[ (\cM(-;A\hom B),\cM(-;A)) \too \cM(-;B). \]
\end{enumerate}

From here, the theory of presentations proceeds as before, yielding a tower of adjunctions.
We can also treat the non-symmetric case using similar ideas; see \cref{ex:moncat-pres}.

\begin{props}
As an example, let us try to reproduce the uniqueness of antipodes calculation from \cref{sec:intro}.
We have already mentioned the theory of a bimonoid in \ref{fig:smc-bimonoid}; an antipode augments this by a generating morphism $i:A\to A$ and the axioms
\begin{align*}
  x:A &\types \match_\tensor(\comult(x),uv.m(u,i(v))) \equiv \match_\one(\counit(x),e) :A\\
  x:A &\types \match_\tensor(\comult(x),uv.m(i(u),v)) \equiv \match_\one(\counit(x),e) :A
\end{align*}
Thus, let us include these and also another antipode $j:A\to A$.

[TODO]
\end{props}


\subsection*{Exercises}

\begin{ex}\label{ex:smc}
  Finish the theory of \cref{sec:shuffles}: prove the admissibility of substitution, state the $\beta$- and $\eta$-conversion rules, and prove the initiality theorem.
\end{ex}

\begin{ex}\label{ex:multicat-day}
  Suppose \cM is a symmetric multicategory and \cC is a cocomplete closed symmetric monoidal category, regarded as a multicategory.
  Show that the symmetric multicategory constructed in \cref{thm:multicat-day} is in fact a closed symmetric monoidal category.
  (In fact, it is the \textbf{Day convolution}~\cite{day:closed} monoidal category constructed from $\catctx\cM$ and $\cC$.)
\end{ex}

\begin{ex}\label{ex:moncat-pres}
  Define 1-skeleta for non-symmetric monoidal categories, and generalize the initiality theorems of \cref{sec:multicat-moncat,sec:multicat-prod-coprod} to a tower of adjunctions involving an appropriate kind of presentation.
\end{ex}

\begin{ex}\label{ex:smc-usage}
  Another approach to linear type theory is to annotate some types in the context with an ``unused'' marker such as $(-)^0$, and allow weakening of ``unused'' types.
  Thus we could have for instance $x:A^0,y:B,z:C^0 \types y:B$, since $x$ and $z$ are marked as unused.
  Two of these contexts $\Gamma$ and $\Delta$ can be \emph{merged} if they contain the same types in the same order, and each type is used (the opposite of unused) in at most one of them; in that case they merge to a context $\Gamma\merge\Delta$ containing the same types again, with those used that are used in either $\Gamma$ or $\Delta$.
  For instance, $(A^0,B,C^0)\merge(A,B^0,C^0) = (A,B,C^0)$.
  \begin{enumerate}
  \item Formulate a type theory containing $\tensor,\times,+,\hom$ using contexts with usage markers and merging rather than concatenation.
    For instance, the rule $\tensorI$ should be
    \[ \inferrule{\Gamma\types M:A \\ \Delta\types N:B}{\Gamma\merge\Delta \types \tpair M N : A\tensor B.}\]
    Prove that exchange, and weakening for unused types, are admissible and functorial, by pushing them up the entire derivation as we did in the cartesian case in \cref{sec:stlc}.
  \item Define a corresponding multicategory-like structure whose domains are lists with usage markers, and establish a correspondence of some sort with symmetric monoidal categories.
  \item Prove an initiality theorem.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:semicart-relevance-strucadm}
  Is it possible to formulate a theory for semicartesian or relevance monoidal categories in which the appropriate structural rules are admissible?
\end{ex}

TODO: \url{https://nforum.ncatlab.org/discussion/8622/church-numerals-are-realizers/}?

\ChapterExercises


% Local Variables:
% TeX-master: "catlog"
% End: