old-prop.tex

Now, if our terms are not simply representations of derivations, then we need to explain what terms \emph{are} before we explain what they mean.
For this purpose we define the class of \emph{pre-terms}, which have a type and a context but may not respect the linearity of the inputs.
The pre-terms, being syntax, are freely generated in an appropriate sense, so we can describe them using an auxiliary judgment $\Gamma \types^\fL M\pc A$.
The intent is that we will eventually judge $\Gamma \types (M_1,\dots,M_n):(A_1,\dots,A_n)$ where each $M_i$ is a pre-term such that $\Gamma \types M_i\pc A_i$.
We will also need to include pre-terms with no type at all, so we also include a judgment $\Gamma \types^\fL M\pc ()$ for this purpose.
In both cases the annotation \fL is a finite subset of \fA indicating which labels might have been used in the terms $M_i,N_i$, to avoid duplication.

The rules for these judgments are shown in \cref{fig:pre-terms}.
It may be tempting to require in the generator rule that all label sets $\fL_i$ in the premises should be disjoint, but this is \emph{not} correct.
For instance, if $f:A\to (B,C)$ and $g:(B,C) \to D$, the composite $g \circ_{(B,C)} f$ will be represented by the pre-term
\begin{mathpar}
  \inferrule*{
    x:A \types^{\fa} f^\fa_1(x)\pc B \\
    x:A \types^{\fa} f^\fa_2(x)\pc C \\
    g\in \cG(B,C;D)\\
    \fb\notin\{\fa\}
  }{
    x:A \types^{\{\fa,\fb\}} g^\fb(f^\fa_1(x),f^\fa_2(x)):D
  }
\end{mathpar}
in which the label \fa appears in multiple premises.
All that matters is that the \emph{new} label being introduced to mark $g$ has not been used before.

We allow an arbitrary finite set of labels in the ``variable'' rule to ensure that the pre-term judgment is closed under adding finitely many more unused labels.
(This can be proved by an easy induction.)
This makes some things more convenient to state, and doesn't matter because \fA is infinite so there will always be fresh labels available.

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{\fL\finsubset\fA \\ \fa\notin\fL}{\Gamma,x:A \types^{\fL\cup\{\fa\}} x^\fa\pc A}\and
    \inferrule{
      \Gamma \types^{\fL_1} M_1\pc A_1 \\ \Gamma\types^{\fL_2} M_2\pc A_2 \\ \cdots \\ \Gamma\types^{\fL_n} M_n\pc A_n \\\\
      f\in \cG(A_1,\dots,A_n; B_1,\dots,B_m)\\ 1\le j\le m \\ \forall i(\fa \notin \fL_i)
    }{
      \Gamma \types^{\fL_1\cup\cdots\cup\fL_n \cup \{\fa\}} f_j^\fa(M_1,\dots,M_n)\pc B_j
    }\and
    \inferrule{
      \Gamma \types^{\fL_1} M_1\pc A_1 \\ \Gamma\types^{\fL_2} M_2\pc A_2 \\ \cdots \\ \Gamma\types^{\fL_n} M_n\pc A_n \\\\
      f\in \cG(A_1,\dots,A_n; \cdot ) \\ \forall i(\fa \notin \fL_i)
    }{
      \Gamma \types^{\fL_1\cup\cdots\cup\fL_n \cup \{\fa\}} f^\fa(M_1,\dots,M_n)\pc ()
    }\and
  \end{mathpar}
  \caption{Rules for pre-terms}
  \label{fig:pre-terms}
\end{figure}

Next we give the rules for the term judgment.
To incorporate morphisms with codomain $()$, we write the judgment as
\[\Gamma \types^\fL (M_1,\dots,M_m\mid N_1,\dots,N_n):(A_1,\dots,A_m)\]
with the intended invariants that $\Gamma\types^{\fL} M_i\pc A_i$ for each $i$ and $\Gamma\types^{\fL} N_j\pc ()$ for each $j$.
Like the pre-term judgment, the term judgment is closed under adding finitely many more unused labels.
If $n=0$ we write simply $(M_1,\dots,M_m)$, omitting the $|$, and if $m=1$ as well we may omit the parentheses.
When pre-terms $M_i$ and $N_j$ appear in a valid term judgment, we refer to them as \textbf{terms}, and we refer to the $N_j$'s in particular as \textbf{null terms}.

We write $\vec M$ for a list of pre-terms, $\vec{x}$ for a list of variables, and $\vec M,N$ for concatenation thereof.
We use capital Greek letters $\Gamma,\Delta,\dots$ both for \emph{contexts} (lists of types with assigned variables such as $x:A,y:B$) and for simple lists of types; the latter can be made into a context by supposing variables $\vec{x}:\Gamma$, or appear as the consequent with assigned terms $\vec{M}:\Gamma$.
Finally, if $f\in\cG(A_1,\dots,A_n;B_1,\dots,B_m)$ we write $\vec{f}^\fa(\vec{M})$ for the list of pre-terms
\[(f_1^\fa(M_1,\dots,M_n),f_2^\fa(M_1,\dots,M_n),\dots,f_m^\fa(M_1,\dots,M_n))\]
where each $M_i \pc A_i$.

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{
      x_1:A_1,\dots,x_n:A_n\types^\fL (M_1,\dots,M_m\mid Z_1,\dots,Z_p):(B_1,\dots,B_m)\\
      \sigma\in \Sigma_n \\ \tau\in\Sigma_m \\ \rho\in\Sigma_p
    }{
      x_{\sigma 1}:A_{\sigma 1},\dots,x_{\sigma n}:A_{\sigma n}\types^\fL (M_{\tau 1},\dots,M_{\tau m}\mid Z_{\rho 1},\dots,Z_{\rho p}):(B_{\tau 1},\dots,B_{\tau m})
    }\and
    \inferrule{\fL\finsubset\fA}{() \types^{\fL} ():()}\and
    \inferrule{\Gamma\types^\fL (\vec{M}\mid \vec{Z}):\Delta\\
      \types A\type\\
      \fa\notin\fL
    }{
      \Gamma,x:A\types^{\fL\cup\{\fa\}} (\vec{M},x^\fa\mid \vec{Z}):(\Delta,A)
    }\and
    \inferrule{
      \Gamma\types^\fL (\vec M,\vec N\mid\vec{Z}):(\Xi,\Psi) \\
      f\in\cG(\Psi; \Delta)\\
      |\Delta|>0\\
      \fa\notin\fL
    }{
      \Gamma \types^{\fL\cup \{\fa\}} (\vec M,\vec f^\fa(\vec N)\mid\vec{Z}):(\Xi,\Delta)
    }\and
    \inferrule{
      \Gamma\types^\fL (\vec M,\vec N\mid\vec{Z}):(\Xi,\Psi) \\
      f\in\cG(\Psi; ())\\
      \fa\notin\fL
    }{
      \Gamma \types^{\fL\cup\{\fa\}} (\vec M\mid\vec{Z},f^\fa(\vec N)):\Xi
    }\and
  \end{mathpar}
  \caption{Rules for terms}
  \label{fig:cl-smc-terms}
\end{figure}

With these notations, the rules for the term judgment are shown in \cref{fig:cl-smc-terms}.
For clarity, we have made the exchange rule explicit at the beginning.
Note that these rules are exactly the rules of the type theory for posetal props \cref{sec:proppos-smpos}, with the additional term annotations.
Moreover, when we annotate the two problematic derivations discussed above, we obtain the same terms.
\begin{mathpar}
  \inferrule*[Right=$g$]{
    \inferrule*{
      \inferrule*[Right=$f$]{
        \inferrule*{\inferrule*{ }{()\types():()}}{x:A\types x:A}
      }{
        x:A\types f(x):B
      }}{
      x:A,y:C\types (f(x),y):(B,C)
    }}{
    x:A,y:C\types (f(x),g(y)):(B,D)
  }\and
  \inferrule*[Right=$f$]{
    \inferrule*{
      \inferrule*[Right=$g$]{
        \inferrule*{\inferrule*{ }{()\types():()}}{y:C\types y:C}
      }{
        y:C\types g(y):D
      }}{
      x:A,y:C\types (x,g(y)):(A,D)
    }}{
    x:A,y:C\types (f(x),g(y)):(B,D)
  }\and
\end{mathpar}

We now commence the metatheoretic analysis.

\begin{lem}
  If $\Gamma\types^\fL (M_1,\dots,M_m\mid N_1,\dots,N_n):(B_1,\dots,B_m)$ is derivable, then so are $\Gamma\types^{\fL} M_i\pc B_i$ and $\Gamma\types^{\fL} N_j\pc ()$ for each $i,j$.
\end{lem}
\begin{proof}
  A straightforward induction over derivations.
\end{proof}

\begin{lem}\label{thm:preterm-subadm}
  The following rule of substitution into pre-terms is admissible:
  \begin{mathpar}
    \inferrule{
      \Gamma \types^{\fM} N_1\pc A_1 \\ \cdots \\ \Gamma\types^{\fM} N_n\pc A_n\\\\
      \Phi,y_1:A_1,\dots,y_n,A_n \types^\fL M\pc B\\
      \fL\cap\fM = \emptyset
    }{
      \Gamma,\Phi \types^{\fL\cup\fM} M[N_1/y_1,\dots,N_n/y_n]\pc B
    }
  \end{mathpar}
\end{lem}
\begin{proof}
  We induct over the derivation of $\Phi,y:A \types^\fL M\pc B$.
  In almost all cases we simply apply the inductive hypothesis to the premise, thereby defining the meaning of substitution on pre-terms by recursing through the structure as usual.
  We require $\fL\cap\fM=\emptyset$ so that the rules that introduce new labels can still be re-applied to the substituted premise, since they require that their new label be fresh.

  As usual, the one rule that behaves differently is $\Gamma,x:A \types^{\fL} x^\fa\pc A$ when $x=y$.
  In this case the result of substitution is just $N$.
\end{proof}

We may write $M[\vec N/\vec y]$ as a shorthand for $M[N_1/y_1,\dots,N_n/y_n]$.
The requirement of label disjointness in \cref{thm:preterm-subadm} means that we cannot decompose these ``simultaneous substitutions'' into iterated single substitutions.
For instance, if $N_1$ and $N_2$ share labels, then \cref{thm:preterm-subadm} would not justify $M[N_1/y_1][N_2/y_2]$.

\begin{lem}\label{thm:prop-subadm}
  Substitution for terms (i.e.\ the cut rule for derivations) is admissible:
  \[\inferrule{
    \Gamma\types^\fL(\vec M,\vec N\mid\vec Z):(\Xi,\Psi) \\
    \vec y:\Psi,\Phi \types^\fM (\vec P\mid\vec W):\Delta\\
    \fM\cap\fL=\emptyset
  }{
    \Gamma,\Phi \types^{\fM\cup\fL} (\vec M, \vec P[\vec N/\vec y] \mid \vec Z, \vec W[\vec N/\vec y]):(\Xi,\Delta)
  }\]
\end{lem}
\begin{proof}
  As is usual for natural deductions, a very straightforward induction.
  Note that the requirement $\fM\cap\fL=\emptyset$ is a generalization of the requirement $\fa\notin\fL$ appearing in the primitive rules.
\end{proof}

We define the \textbf{height} of a derivation to be the number of rules appearing in it \emph{other} than the exchange rule.
The following ``invertibility'' lemma is key to the initiality theorem.

\begin{lem}\label{thm:prop-invertible}
  If we have a derivation of a given sequent \sQ, and an instance \cR of a rule whose conclusion is \sQ, then we can construct a derivation of \sQ that ends with \cR and has the same height as the given one.
\end{lem}
\begin{proof}
  This is trivially true for the exchange rule (since it supplies its own inverses and contributes no height) and for the trivial rule $()\types ():()$.
  For all the other rules \cR, suppose the given derivation ends with a different rule application $\cS$ (disregarding any exchanges in between).
  Now note that each rule introduces a new label and introduces exactly those terms in the judgment whose outer connective has that label.
  Therefore, the rule applications $\cR$ and $\cS$, being different, must introduce different labels, and therefore introduce \emph{disjoint} sets of terms.
  (This is where the argument would fail without labels.)

  It follows that the premise of \cS, say $\sQ'$, is also a conclusion of some instance $\cR'$ of the same rule as \cR.
  Therefore, we can apply the inductive hypothesis to obtain a derivation of this premise ending with $\cR'$, whose premise is $\sQ''$ say.
  Now by the same disjointness argument, we can apply an instance $\cS'$ of the same rule as \cS to $\sQ''$, and then $\cR$ to the conclusion of that rule, obtaining our desired derivation.
  The height is clearly preserved.
\end{proof}

That proof was written very abstractly, so consider the following example with $f\in\cG(A;D,E)$ and $g\in\cG(B;C,F)$.
We omit to write exchange rules, as well as the obvious variable rules at the top.
\begin{mathpar}
  \inferrule*[Right=$g$]{
    \inferrule*[Right=$f$]{
      x:A,y:B \types (y,x):(B,A)
    }{
      x:A,y:B \types (y,f_2(x),f_1(x)):(B,E,D)
    }
  }{
    x:A,y:B \types (g_1(y),f_2(x),g_2(y),f_1(x)):(C,E,F,D)
  }
\end{mathpar}
The conclusion of this rule is (modulo exchange) the conclusion of an instance of the $f$-generator rule.
Now the $g$-terms introduced by the actual rule that leads to this conclusion are disjoint from the $f$-terms that would be introduced by this $f$-generator rule.
Thus, by induction the premise $x:A,y:B \types (y,f_2(x),f_1(x)):(B,E,D)$ has a derivation of the same height ending with the $f$-generator rule; in this simple case that is in fact the derivation of it that we were given.
Now we can apply the $g$-generator rule to the premise of \emph{that} rule, namely $x:A,y:B C \types (y,x):(B C,A)$, and then follow it by the $f$-generator rule, obtaining the following derviation:
\begin{mathpar}
  \inferrule*[Right=$f$]{
    \inferrule*[Right=$g$]{
      x:A,y:B \types (y,x):(B C,A)
    }{
      x:A,y:B C \types (g_1(y),g_2(y),x):(C,F,A)
    }
  }{
    x:A,y:B \types (g_1(y),f_2(x),g_2(y),f_1(x)):(C,E,F,D)
  }
\end{mathpar}

\begin{thm}\label{thm:prop-initial}
  The free prop on a polygraph can be presented using this type theory: its morphisms $\Gamma\to\Delta$ are the \emph{pairs $(\vec M,\vec Z)$ of lists of terms} such that $\Gamma\types^\fL (M_1,\dots,M_n \mid Z_1,\dots,Z_p):\Delta$ is derivable for some $\fL\finsubset\fA$, modulo the equivalence relation generated by (a) permutation of labels and (b) permutation of the null terms $\vec Z$.
  In particular, if two derivations give the same lists of pre-terms, we stipulate that only one morphism results.
\end{thm}
\begin{proof}
  \cref{thm:prop-subadm} tells us how to compose morphisms.
  Associativity, unitality, and equivariance follow as usual, since substitution into pre-terms is basically ordinary substitution.
  In particular, these axioms hold as syntactic equalities of pre-terms.

  For the interchange rule, suppose given derivations of $\Gamma\types (\vec M\mid\vec Z):\Delta$ and $\Phi\types (\vec N\mid\vec W):\Xi$.
  We can then substitute them along $()$ in either order to get
  \begin{align*}
    \Gamma,\Phi &\types (\vec M,\vec N\mid \vec Z,\vec W):\Delta,\Xi\\
    \Phi,\Gamma &\types (\vec N,\vec M\mid \vec W,\vec Z):\Xi,\Delta\\
\intertext{Applying exchange to the second, we obtain}
    \Gamma,\Phi &\types (\vec M,\vec N\mid \vec W,\vec Z):\Delta,\Xi
  \end{align*}
  and we have $(\vec M,\vec N\mid \vec Z,\vec W) \equiv (\vec M,\vec N\mid \vec W,\vec Z)$ by the permutation condition (b).
  In particular, unlike the other axioms, interchange doesn't hold as an on-the-nose equality of syntax.

  In any case, we now have a prop $\F\bProp\cG$.
  We define the inclusion of polygraphs $\cG\to \F\bProp\cG$ by sending $f\in\cG(\Gamma,\Delta)$ to $\vec x:\Gamma \types (\vec f^\fa(\vec x)):\Delta$ (or to $\vec x:\Gamma \types (\,\mid\vec f^\fa(\vec x)):()$ if $\Delta=()$), for some $\fa\in\fA$.
  This is independent of the choice of \fa due to the permutation condition (a).

  Now suppose \cM is any prop and $P:\cG\to\cM$ is a morphism of polygraphs.
  We extend $P$ to the prop $\F\bProp\cG$ by induction on derivations.
  This is straightforward using the prop structure of \cM; the nontrivial thing is showing that the result depends only on the pre-term judgment rather than on the particular derivation.
  This is the purpose of \cref{thm:prop-invertible}, which we apply as follows.

  Suppose we have two derivations $\sD_1$ and $\sD_2$ of the same sequent $\sQ$, ending with rules $\cR_1$ and $\cR_2$ with premises $\sQ_1$ and $\sQ_2$ respectively.
  By disjointness of pre-terms as in the proof of \cref{thm:prop-invertible}, we can say that $\sQ_1$ is a conclusion of an instance of $\cR_2$, and similarly $\sQ_2$ is a conclusion of an instance of $\cR_1$.
  By \cref{thm:prop-invertible}, therefore, $\sQ_1$ has a derivation $\sD_1'$ of the same height ending with $\sR_2$, while $\sQ_2$ has a derivation $\sD_2'$ of the same height ending with $\sR_1$.
  Moreover, up to exchange (as always) the premise of these two ending rules must be the same sequent $\sQ_3$.
  By induction (which is applicable since the heights have been preserved), the given derivations of $\sQ_1$ and $\sQ_2$ yield the same morphism in \cM as these other derivations $\sD_1'$ and $\sD_2'$.

  Thus, it will suffice to show that once the sequent $\sQ_3$ is interpreted according to some particular derivation of it, we obtain the same interpretation of $\sQ$ by deriving it in the following two ways:
  \begin{mathpar}
    \inferrule*[Right=$\cR_1$]{\inferrule*[Right=$\cR_2$]{\vdots\\\\\sQ_3}{\sQ_1}}{\sQ}\and
    \inferrule*[Right=$\cR_2$]{\inferrule*[Right=$\cR_1$]{\vdots\\\\\sQ_3}{\sQ_2}}{\sQ}\and
  \end{mathpar}
  This follows from the associativity and interchange rules in \cM.

  Thus we have a map of polygraphs $\F\bProp\cG\to\cM$, which extends $P$ by construction.
  To see that it is the unique such extension that could be a prop functor, note that every primitive rule is essentially an instance of identity or cut.
  In the former case, its image in $\cM$ must also be an identity.
  In the latter case, we may inductively suppose the image in \cM of its first input is already uniquely determined, while its second input is either an identity (hence determined) or a generating morphism in \cG, and the images of the latter are determined by $P$.
  (Here we use again the imposed invariance (a) under permutation of labels, since otherwise $P$ would only determine the images of the generators with the particular labels we chose to define the inclusion $\cG\to\F\bProp\cG$.)
  Thus, their composite is also uniquely determined.

  Finally, we must show that $\F\bProp\cG\to\cM$ actually \emph{is} a prop functor, i.e.\ it preserves identities and composition.
  Identities are immediate, while composition follows as usual by inductively considering the definition of composition (i.e.\ substitution) in $\F\bProp\cG$.
\end{proof}

We can extend this type theory for props to a type theory for symmetric monoidal categories by introducing tensors and units, as we did in the posetal case.
For this purpose we reformulate the sequent calculus rules for these as a natural deduction, introducing the new rules for pre-terms and terms shown in \cref{fig:prop-smc-preterms,fig:prop-smc-terms}.

% \begin{figure}
%   \centering
%   \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}
%     \inferrule{ }{()\types()}\and
%     \inferrule{\Gamma\types\Delta\\ \types A\type}{\Gamma,A\types \Delta,A}\and
%     \inferrule{\Gamma\types\Xi,\Psi \\ f\in\cG(\Psi; \Delta)}{\Gamma \types \Delta,\Xi}\and
%     \inferrule{\Gamma\types \Delta,A,B}{\Gamma\types \Delta,A\tensor B}\;\tensorI\and
%     % \inferrule{\Xi\types\Phi,\Psi,A\tensor B \\ \Gamma,\Psi,A,B\types \Delta}{\Gamma,\Xi\types \Phi,\Delta}\;\tensorE\and
%     \inferrule{\Gamma\types \Delta,A\tensor B}{\Gamma\types \Delta,A,B}\;\tensorE\and
%     \inferrule{\Gamma\types\Delta}{\Gamma\types\Delta,\one}\;\one I\and
%     % \inferrule{\Xi\types \Phi,\Psi,\one \\ \Gamma,\Psi\types\Delta}{\Gamma,\Xi\types\Phi,\Delta}\;\one E\and
%     \inferrule{\Gamma\types\Delta,\one}{\Gamma\types\Delta}\;\one E\and
%   \end{mathpar}
%   \caption{Classical natural deduction for symmetric monoidal categories}
%   \label{fig:clnatded-smc}
% \end{figure}

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{
      \Gamma\types^{\fL_1} M\pc A \\ \Gamma\types^{\fL_2} N\pc B \\
      \fa\notin \fL_1\cup\fL_2
    }{
      \Gamma\types^{\fL_1\cup\fL_2\cup\{\fa\}} \tpair{M}{N}^\fa \pc A\tensor B
    }\and
    \inferrule{\fL \finsubset \fA \\ \fa\notin\fL}{\Gamma\types^{\fL\cup\{\fa\}} \ott^\fa\pc\one}\and
    \inferrule{\Gamma\types^\fL M\pc A\tensor B \\ \fa\notin\fL}{\Gamma\types^{\fL\cup\{\fa\}} \varpi_1^\fa(M) \pc A}\and
    \inferrule{\Gamma\types^\fL M\pc A\tensor B \\ \fa\notin\fL}{\Gamma\types^{\fL\cup\{\fa\}} \varpi_2^\fa(M) \pc B}\and
    \inferrule{\Gamma\types^\fL M\pc \one \\ \fa\notin\fL}{\Gamma\types^{\fL\cup\{\fa\}} \cancel{M}^\fa:()}\and
  \end{mathpar}
  \caption{Pre-terms for symmetric monoidal categories}
  \label{fig:prop-smc-preterms}
\end{figure}

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{
      \Gamma\types^\fL (\vec{M},N,P\mid\vec{Z}):(\Delta,A,B)\\
      \fa\notin\fL
    }{
      \Gamma\types^{\fL\cup\{\fa\}} (\vec{M},\tpair{N}{P}^\fa \mid\vec{Z}):(\Delta,A\tensor B)
    }\;\tensorI\and
    \inferrule{
      \Gamma\types^\fL (\vec{M},P\mid\vec{Z}):(\Delta,A\tensor B)\\
      \fa\notin\fL
    }{
      \Gamma\types^{\fL\cup\{\fa\}} (\vec{M},\varpi_1^\fa(P),\varpi_2^\fa(P)\mid\vec{Z}):(\Delta,A,B)
    }\;\tensorE\\
    \inferrule{
      \Gamma\types^\fL(\vec M\mid\vec Z):\Delta\\
      \fa\notin\fL
    }{
      \Gamma\types^{\fL\cup\{\fa\}} (\vec M,\ott^\fa\mid\vec Z):(\Delta,\one)
    }\;\one I\and
    \inferrule{
      \Gamma\types^\fL(\vec M,N\mid\vec Z):(\Delta,\one)\\
      \fa\notin\fL
    }{
      \Gamma\types^{\fL\cup\{\fa\}}(\vec M\mid \cancel{N}^\fa,\vec Z):\Delta
    }\;\one E\and
  \end{mathpar}
  \caption{Terms for symmetric monoidal categories}
  \label{fig:prop-smc-terms}
\end{figure}

Now we need to deal with the $\beta$ and $\eta$ equalities, by introducing an equality judgment.
This takes the form
\[\Gamma \types^{\fL;\fM} (\vec M\mid\vec Z)\equiv (\vec N\mid\vec W) :(\vec B)\]
which should respect the invariants
\begin{alignat*}{2}
  \Gamma&\types^{\fL} M_i\pc B_i &\qquad
  \Gamma&\types^{\fL} Z_j\pc ()\\
  \Gamma&\types^{\fM} N_i\pc B_i &\qquad
  \Gamma&\types^{\fM} W_j\pc ()
\end{alignat*}
Note that these may not be well-typed term judgments.
% TODO: Should they be?

We assert that this relation $\equiv$ is a congruence on lists of pre-terms with respect to concatenation, substitution, and permutation, and that it is invariant under permutations of the label set \fA \emph{separately on each side}.
That is, there is no requirement that the actual labels used on the two sides of $\equiv$ match up; to the eyes of $\equiv$, the label annotations simply define a partition of the ``label occurrences'' in a list of pre-terms.
(We do, of course, have to keep track of individual labels at the level of pre-terms; it's only after they are grouped into lists that we can ignore the identity of the labels.)
% TODO: Do we need to worry more about what happens to the labels here?
We assert moreover that $\equiv$ allows us to permute the second parts of pre-term lists freely:
\[ (\vec M \mid \vec{Z}) \equiv (\vec M \mid \vec{\sigma Z})\]
Thus, it incorporates the permutation quotients (a) and (b) from \cref{thm:prop-initial}.

Relative to the above closure conditions, $\equiv$ is generated by the following relations on individual pre-terms (occurring anywhere in a list):
\begin{mathpar}
  \varpi_1^\fa(\tpair M N^\fb) \equiv M\and
  \varpi_2^\fa(\tpair M N^\fb) \equiv N\and
  \tpair{\varpi_1^\fa(P)}{\varpi_2^\fa(P)}^\fb \equiv P\and
  \cancel{\ott^\fa}^\fb \equiv ()\and
\end{mathpar}
and also the following relation on lists:
\begin{mathpar}
  (\vec M,\ott^\fa \mid \vec Z,\cancel{W}^\fb) \equiv (\vec M,W\mid \vec Z)\and
\end{mathpar}

We leave it to the reader to extend the metatheory to deal with $\tensor$ and $\one$ and prove the initiality theorem; there is very little difference with the prop case.