props.tex

\documentclass{article}
\usepackage{mathpartir,cancel,cmll}
\newif\ifcref\creftrue
\input{decls}
\usepackage{mathpartir}
\makeatletter
\autodefs{\bSet\bPoset\bRelGr\bCat\bGr\bmSLat\ftype\bPrCat\bCoprCat\bMCat\bMGr\bMPos\bRelMGr\bMonPos\bMonCat\bSMPos\bSMC\bProp}
\def\tr{\mathrm{tr}}
\let\sect\section
\def\idfunc{\mathsf{id}}
\def\finsubset{\subset_{\mathrm{fin}}}
% judgments
\let\types\vdash
\def\type{\;\ftype}
\newcommand{\pc}{\mathrel{\mathord{:}?}}
\newcommand{\atom}{\mathrel{\downarrow}}
\newcommand{\can}{\mathrel{\uparrow}}
\newcommand{\atomcan}{\ensuremath{\mathord{\downarrow\uparrow}}}
\newcommand{\focus}[1]{[#1]}
\newcommand{\postcsym}[1]{#1\mathord{\circ}}
\newcommand{\postc}[2]{\postcsym{#1}(#2)}
\newcommand{\precsym}[1]{\mathord{\circ}#1}
\renewcommand{\prec}[2]{(#1)\precsym{#2}}
% substitution
\newcommand{\hsub}[1]{\llbracket #1\rrbracket}
\newcommand{\hid}[1]{\mathbbb{id}_{#1}}
% free functors
\newcommand{\F}[1]{\mathfrak{F}_{#1}}
% meet
\let\meet\wedge
\def\meetL{\mathord{\meet}L}
\def\meetR{\mathord{\meet}R}
\def\meetE{\mathord{\meet}E}
\def\meetI{\mathord{\meet}I}
% join
\let\join\vee
\def\joinL{\mathord{\join}L}
\def\joinR{\mathord{\join}R}
\def\joinE{\mathord{\join}E}
\def\joinI{\mathord{\join}I}
% unit
\def\unit{\mathbf{1}}
\def\ttt{\mathsf{tt}}
% product
\def\timesE{\ensuremath{\mathord{\times}E}}
\def\timesI{\ensuremath{\mathord{\times}I}}
\def\pair#1#2{\langle #1,#2\rangle}
% coproduct
\def\plusE{\mathord{+}E}
\def\plusI{\mathord{+}I}
\def\inl{\mathsf{inl}}
\def\inr{\mathsf{inr}}
\def\case{\mathsf{case}}
% empty
\def\emptyt{\mathbf{0}}
\def\abort{\mathsf{abort}}
% one
\def\one{\mathbf{1}}
\def\discard#1in{\mathsf{discard}\; #1 \; \mathsf{in} \;}
% tensor
\let\tensor\otimes
\def\tensorL{\mathord{\tensor}L}
\def\tensorR{\mathord{\tensor}R}
\def\tensorI{\mathord{\tensor}I}
\def\tensorE{\mathord{\tensor}E}
\let\bigtensor\bigotimes
\def\flet#1:{\mathsf{let}\;#1 \@ifnextchar:\@fletdoublecolon\@fletsinglecolon}
\def\fletp#1:{\mathsf{let}'\;#1 \@ifnextchar:\@fletdoublecolon\@fletsinglecolon}
\def\@fletdoublecolon:=#1in{\Coloneqq #1\;\mathsf{in}\;}
\def\@fletsinglecolon=#1in{\coloneqq #1\;\mathsf{in}\;}
\makeatother

\title{A type theory for props}
\author{Michael Shulman}
\begin{document}

\maketitle

\section{Posetal props}
\label{sec:posetal-props}

Let us consider sequents $\Gamma\types\Delta$ where the commas on both sides are intended to represent the \emph{same} tensor product $\tensor$.
For simplicity, we assume this tensor product is symmetric, so that we have an exchange rule on both sides.
This leads us to consider different identity and cut rules than for linear logic (in fact, two identity rules):
\begin{mathpar}
  \inferrule*{ }{()\types()}\and
  \inferrule*{\Gamma\types\Delta}{\Gamma,A\types \Delta,A}\and
  \inferrule*[Right=cut]{\Gamma\types\Xi,\Psi \\ \Psi,\Phi \types \Delta}{\Gamma,\Phi \types \Delta,\Xi}
\end{mathpar}
As always, of course, we intend for the cut rule to be admissible, but writing down at this point what it should be helps us build it into other rules appropriately.

To prove an initiality theorem, we need an appropriate categorical structure.
We define a \textbf{prop} to be a symmetric polygraph \cP (that is, a set of objects together with sets of arrows $\cP(A_1,\dots A_n;B_1,\dots,B_m)$, and appropriate symmetric group actions) together with the following data:
\begin{enumerate}
\item A morphism $\idfunc_{()}:()\to ()$.
\item For every $A\in\cP$, a morphism $\idfunc_A (A)\to (A)$.
  % For every $f:\Gamma\to\Delta$ and object $A$, a morphism $(f,\idfunc_A):(\Gamma,A) \to (\Delta,A)$.
  % By induction from this and the previous, we have $\idfunc_{\Gamma} :\Gamma\to\Gamma$ for any $\Gamma$.
\item For every $f:\Gamma\to (\Xi,\Psi)$ and $g:(\Psi,\Phi)\to \Delta$, a composite $g\circ_\Psi f : (\Gamma,\Phi) \to (\Xi,\Delta)$.
% \item Identities are invariant under permutation: $\sigma\idfunc_{\Gamma}\sigma = \idfunc_{\sigma\Gamma}$.
\item Composition is invariant under permutation: $\tau(g\circ_\Psi f)\sigma = (\tau g)\circ_\Psi (f\sigma)$ and $g\sigma \circ_\Psi f = g\circ_{\sigma \Psi} \sigma f$.
\item Composition is unital:
  % $g\circ_\Psi \idfunc_\Psi = g$ and $\idfunc_\Psi\circ_\Psi f = f$.
  $g\circ_A \idfunc_A = g$ and $\idfunc_A\circ_A f = f$.
\item Composition is associative: given $f:\Gamma\to (\Xi,\Theta,\Psi)$ and $g:(\Psi,\Phi)\to (\Delta,\Upsilon)$ and $h:(\Upsilon,\Theta,\Lambda)\to \Omega$, we have
  \[h \circ_{\Upsilon,\Theta} (g\circ_\Psi f) = (h\circ_\Upsilon g) \circ_{\Theta,\Psi} f \qquad \text{(as morphisms} (\Gamma,\Phi,\Lambda) \to (\Xi,\Delta,\Omega). \]
\item Composition is interchanging: $g\circ_{()}f = f\circ_{()}g$ (modulo a symmetry action).
\end{enumerate}
By composing along empty lists, we get a ``tensor product'' of morphisms: if $f:\Gamma\to\Xi$ and $g:\Phi\to\Delta$, then $g\circ_{()}f : (\Gamma,\Phi) \to (\Xi,\Delta)$.
(This sort of operation is what distinguishes a prop from a ``properad''.)
In particular, we can produce identity morphisms for lists: $\idfunc_{(A,B)} = \idfunc_A \circ_{()} \idfunc_B$ and so on.

Similarly we have $f\circ_{()}g : (\Phi,\Gamma) \to (\Delta,\Xi)$, and the interchange axiom means that these two morphisms are related by the appropriate symmetric group actions.
In the special case when $\Gamma=\Phi=\Xi=\Delta=()$, the Eckmann--Hilton argument implies that the morphisms $()\to ()$ form a commutative monoid; thus our props are the original ones of Adams--MacLane~\cite{maclane:natural-assoc,maclane:cat-alg} rather than the ``graphical'' ones of Batanin--Berger~\cite{bb:htapm}.

It may not be obvious that the above axioms do actually give the same notion of prop.
Eventually we will prove this; but in this section we restrict to the posetal case, in which case the axioms are irrelevant.
By a \textbf{posetal prop} we mean a prop in which there is at most one morphism $\Gamma\to\Delta$ for any $\Gamma,\Delta$.
Given a relational polygraph \cG (that is, one with at most one arrow of each type), we define the \textbf{type theory for posetal props under \cG} to have the two identity rules and a Yoneda-ified generator rule:
\begin{mathpar}
  \inferrule{ }{()\types()}\and
  \inferrule{\Gamma\types\Delta}{\Gamma,A\types \Delta,A}\and
  \inferrule{\Gamma\types\Xi,\Psi \\ f\in\cG(\Psi,\Phi; \Delta)}{\Gamma,\Phi \types \Delta,\Xi}
\end{mathpar}

\begin{thm}\label{thm:prop-cutadm}
  For any polygraph \cG, the above cut rule is admissible in the type theory for posetal props under \cG.
\end{thm}
\begin{proof}
  As always, we induct on the derivation of $\Psi,\Phi \types \Delta$.
  \begin{enumerate}
  \item If it is the empty identity rule $()\types()$, then $\Gamma\types\Xi,\Psi$ is just $\Gamma\types\Xi$ and is also the desired conclusion.
  \item If it ends with the other identity rule, then there are two cases.
    \begin{enumerate}
    \item If $A$ is in $\Phi$, then we have $\Phi=\Phi',A$ and $\Delta=\Delta',A$ and a derivation of $\Psi,\Phi'\types\Delta'$.
      Applying the inductive hypothesis to this we get $\Gamma,\Phi'\types \Xi,\Delta'$, and then applying the identity rule again gives the desired conclusion.
    \item If $A$ is in $\Psi$, then we have $\Psi=\Psi',A$ and $\Delta=\Delta',A$ and a derivation of $\Psi',\Phi\types\Delta'$.
      Now we can inductively cut this with the given $\Gamma\types \Xi,A,\Psi'$ along $\Psi'$ to get $\Gamma,\Phi\types \Xi,A,\Delta'$ which is the desired conclusion.
    \end{enumerate}
  \item Finally, suppose $\Psi,\Phi \types \Delta$ ends with the rule for an $f$.
    Thus, we have $\Delta=\Delta_1,\Delta_2$ and $\Psi=\Psi_1,\Psi_2$ and $\Phi=\Phi_1,\Phi_2$, where $f\in\cG(\Psi_2,\Phi_2,\Upsilon;\Delta_1)$ and a given derivation of $\Psi_1,\Phi_1\types \Delta_2,\Upsilon$.
    We first inductively cut the latter with our given $\Gamma\types \Xi,\Psi_1,\Psi_2$ along $\Psi_1$ to get $\Gamma,\Phi_1\types \Xi,\Psi_2,\Delta_2,\Upsilon$, then apply the $f$ rule on $\Psi_2,\Upsilon$ to get the desired $\Gamma,\Phi_1,\Phi_2\types \Xi,\Delta_1,\Delta_2$ as desired.\qedhere
  \end{enumerate}
\end{proof}

\begin{thm}\label{thm:posprop-initial}
  For any relational polygraph \cG, the free posetal prop generated by \cG is described by the type theory for posetal props under \cG: its objects are those of \cG, and we have $\Gamma\le\Delta$ just when $\Gamma\types\Delta$ is derivable.
\end{thm}
\begin{proof}
  \cref{thm:prop-cutadm} implies that these definitions give us a posetal prop $\F\bSMPos\cG$.
  Now if \cM is any other posetal prop and $P:\cG\to\cM$ is a map of relational polygraphs, to extend $P$ to $\F\bSMPos\cG$ it suffices to check that it preserves the relation.
  This follows by an easy induction on the rules.
\end{proof}

Now, there are actually \emph{three} ways we could imagine introducing tensor products in a prop.
Fortunately, they are all equivalent.

\begin{lem}\label{thm:prop-tensor}
  For any two objects $A$ and $B$ in a prop \cP, the following are equivalent.
  \begin{enumerate}
  \item A morphism $(A,B) \to A\tensor B$, precomposition with which defines bijections\label{item:prop-tensor-left}
    \[ \cP(\Gamma,A\tensor B;\Delta) \to \cP(\Gamma,A,B;\Delta) \]
  \item A morphism $A\tensor B \to (A,B)$, postcomposition with which defines bijections\label{item:prop-tensor-right}
    \[ \cP(\Gamma;\Delta,A\tensor B) \to \cP(\Gamma;\Delta,A,B) \]
  \item Morphisms $(A,B) \to A\tensor B$ and $A\tensor B \to (A,B)$ whose composites in both directions
    \begin{gather*}
      A\tensor B \too (A,B)  \too A\tensor B\\
      (A,B)\too A\tensor B \too (A,B)
    \end{gather*}
    are identities.\label{item:prop-tensor-iso}
  \end{enumerate}
\end{lem}
\begin{proof}
  If we have~\ref{item:prop-tensor-iso}, then pre- or post-composing with the other morphism yields the bijections in~\ref{item:prop-tensor-left} and~\ref{item:prop-tensor-right}.
  On the other hand, given~\ref{item:prop-tensor-left}, the identity $(A,B)\to (A,B)$ must be the composite $(A,B)\to A\tensor B \to (A,B)$ for some unique morphism $A\tensor B \to (A,B)$, and the other composite must be the identity since its precomposite with $(A,B)\to A\tensor B$ is $(A,B)\to A\tensor B$; so~\ref{item:prop-tensor-iso} holds.
  (This is basically the Yoneda lemma.)
  The case of~\ref{item:prop-tensor-right} is dual.
\end{proof}

The case with units is similar.

\begin{lem}\label{thm:prop-unit}
  In a prop \cP, the following are equivalent.
  \begin{enumerate}
  \item A morphism $()\to \one$, precomposition with which defines bijections
    \[\cP(\Gamma,\one;\Delta) \to \cP(\Gamma;\Delta).\]
  \item A morphism $\one\to()$, postcomposition with which defines bijections
    \[\cP(\Gamma;\Delta,\one) \to \cP(\Gamma;\Delta).\]
  \item Morphisms $()\to \one$ and $\one\to()$ whose composites in both directions are identities.\qed
  \end{enumerate}
\end{lem}

\begin{thm}\label{thm:prop-smc}
  There is an equivalence between (1) symmetric monoidal categories and (2) props with tensors and units in the sense of \cref{thm:prop-tensor,thm:prop-unit}.
\end{thm}
\begin{proof}
  Given a symmetric monoidal category \cC, we define a prop \cP by
  \[ \cP(A_1,\dots,A_n ; B_1,\dots,B_m) = \cC(A_1\tensor \cdots\tensor A_n, B_1\tensor\cdots\tensor B_m)\]
  or, more succinctly, $\cP(\Gamma;\Delta) = \cC(\bigtensor\Gamma, \bigtensor\Delta)$.
  Of course, $\bigtensor() = \one$.
  The identity rules come from $\idfunc_\one$ and $f\tensor \idfunc_A$, while the composite of $f:\Gamma\to (\Xi,\Psi)$ and $g:(\Psi,\Phi)\to \Delta$ is $(\bigtensor\Xi \tensor g) \circ (f\tensor \bigtensor \Phi)$.
  Of course, this prop has tensors and units quite trivially.

  Conversely, given a prop with tensors and units, we have an underlying category with an object $\one$ and an operation $\tensor$.
  The functoriality of $\tensor$ is defined on $f:A\to A'$ and $g:B\to B'$ as the composite
  \[ A\tensor B \too (A,B) \xto{(f,\idfunc)} (A',B) \xto{(\idfunc,g)} (A',B') \too A'\tensor B'. \]
  The axioms of a prop ensure that this is the same as if we put $f$ and $g$ in the other order (or we could write simply $(f,g)$ using the yet-to-be-defined polycomposition).
  Functoriality is similarly easy.
  For associativity, we have
  \[ ((A\tensor B)\tensor C) \too (A\tensor B,C) \too (A,B,C) \too (A,B\tensor C) \to (A\tensor (B\tensor C)) \]
  and for unitality we have
  \[ (A\tensor \unit) \too (A,\unit) \too (A) \]
  and dually.
  It is straightforward to check that these are natural isomorphisms and satisfy the necessary axioms.
  For symmetry, we use the fact that our prop is a \emph{symmetric} polygraph and act by symmetry on the morphisms $(A,B)\to A\tensor B$ and $A\tensor B\to (A,B)$, obtaining ``inverse isomorphisms'' $(B,A) \to A\tensor B$ and $A\tensor B \to (B,A)$.
  From these we can show $A\tensor B \cong B\tensor A$ and check naturality and the axioms.

  It is straightforward to check that these two constructions are inverses.
\end{proof}

\cref{thm:prop-tensor,thm:prop-unit} give several ways to introduce $\tensor$ and $\unit$ into the type theory of posetal props.
For a sequent calculus, the symmetrical approach is probably the most natural:
\begin{mathpar}
  \inferrule{\Gamma,A,B\types \Delta}{\Gamma,A\tensor B\types \Delta}\;\tensorL\and
  \inferrule{\Gamma\types \Delta,A,B}{\Gamma\types \Delta,A\tensor B}\;\tensorR\and
  \inferrule{\Gamma\types\Delta}{\Gamma,\one\types\Delta}\;\one L\and
  \inferrule{\Gamma\types\Delta}{\Gamma\types\Delta,\one}\;\one R\and
\end{mathpar}
Of course, we also include the identity and generator rules (the former only for base types coming from \cG) and the type judgment:
\begin{mathpar}
  \inferrule{ }{()\types()}\and
  \inferrule{\Gamma\types\Delta\\ A\in\cG}{\Gamma,A\types \Delta,A}\and
  \inferrule{\Gamma\types\Xi,\Psi \\ f\in\cG(\Psi,\Phi; \Delta)}{\Gamma,\Phi \types \Delta,\Xi}\and
  \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}
We call this the \textbf{classical sequent calculus for symmetric monoidal posets under \cG}.
(``Classical'' because we have multiple formulas on both sides, ``posets'' because we are not yet distinguishing derivations or introducing terms.)

\begin{thm}\label{thm:seqcalc-smpos-invertible}
  All the rules for $\tensor$ and $\one$ in the classical sequent calculus for symmetric monoidal posets under \cG are invertible.
\end{thm}
\begin{proof}
  Suppose we have a derivation of $\Gamma,A\tensor B\types \Delta$; we want a derivation of $\Gamma,A,B\types \Delta$.
  We induct on the given derivation.
  \begin{enumerate}
  \item The easy case is when it ends with $\tensorL$ whose premise is what we want.
  \item If it ends with $\tensorL$ acting on another type, or any of $\tensorR$, $\one L$, or $\one R$, then we induct on the premise and then apply that rule to the result.
  \item If it ends with the identity rule for $C$, then since $C\in \cG$ it can't be $A\tensor B$, so we can again induct on the premise and apply the identity rule afterwards.
  \item Finally, if it ends with a generator rule for $f$, then since the domain of $f$ is a list of objects of $\cG$, none of them can be $A\tensor B$; so $A\tensor B$ must be in the sequent that the generator rule cuts with, and we can induct on that and then apply the generator rule.
  \end{enumerate}
  The other rules $\tensorR$, $\one L$, and $\one R$ are similar.
\end{proof}

\begin{thm}\label{thm:seqcalc-smpos-identity}
  The following general identity rule is admissible in the classical sequent calculus for symmetric monoidal posets under \cG:
  \begin{mathpar}
    \inferrule{\Gamma\types\Delta\\ \types A\type}{\Gamma,A\types \Delta,A}\and
  \end{mathpar}
  In particular, since $()\types()$, we have $A\types A$ whenever $\types A\type$.
\end{thm}
\begin{proof}
  We induct on the derivation of $\types A\type$.
  \begin{enumerate}
  \item If it is from \cG, we apply the postulated identity rule.
  \item If it is $\one$, we have the following derivation:
    \begin{mathpar}
      \inferrule*{\inferrule*{\inferrule*{ }{()\types()}}{() \types \one}}{\one\types\one}
    \end{mathpar}
  \item If it is $A_1\tensor A_2$, we have by induction a derivation $\sD_1$ of $\Gamma,A_1\types,\Delta,A_1$, and then (again by induction) a derivation $\sD_2$ of $\Gamma,A_1,A_2\types \Delta,A_1,A_2$.
    Now we augment this in a similar way:
    \begin{equation*}
      \inferrule*{
        \inferrule*{
          \inferrule*{\sD_2\\\\\vdots}{\Gamma,A_1,A_2\types \Delta,A_1,A_2}
        }{
          \Gamma,A_1\tensor A_2\types \Delta,A_1,A_2
        }}{
        \Gamma,A_1\tensor A_2\types \Delta,A_1\tensor A_2
      }\qedhere
    \end{equation*}
  \end{enumerate}
\end{proof}

\begin{thm}\label{thm:seqcalc-smpos-cutadm}
  The prop cut rule is admissible in the classical sequent calculus for symmetric monoidal posets under \cG.
\end{thm}
\begin{proof}
  Suppose given derivations of $\Gamma\types\Xi,\Psi$ and $\Psi,\Phi \types \Delta$; we want to derive $\Gamma,\Phi \types \Delta,\Xi$.
  We induct on the derivation of $\Psi,\Phi \types \Delta$.
  \begin{enumerate}
  \item If it ends with an identity or a generator, we do as in \cref{thm:prop-cutadm}.
  \item If it ends with $\tensorR$ or $\one R$, we can simply apply the inductive hypothesis to cut with the premise of that rule.
  \item If it ends with $\tensorL$, there are two cases.
    If the introduced $A\tensor B$ is in $\Phi$, then we can inductively cut the premise along $\Psi$ again.
  \item On the other hand, if the introduced $A\tensor B$ is in $\Psi$, then our other derivation has the form $\Gamma\types\Xi,\Psi',A\tensor B$.
    Since $\tensorR$ is invertible by \cref{thm:seqcalc-smpos-invertible}, we can also derive $\Gamma\types\Xi,\Psi',A,B$, and then cut with the premise $\Psi',A,B,\Phi \types \Delta$ of our $\tensorL$.
  \item The case of $\one L$ is similar.\qedhere
  \end{enumerate}
\end{proof}

\begin{thm}\label{thm:seqcalc-smpos-initial}
  For any relational polygraph \cG, the free symmetric monoidal poset generated by \cG is described by the classical sequent calculus for symmetric monoidal posets under \cG.
\end{thm}
\begin{proof}
  \cref{thm:seqcalc-smpos-identity,thm:seqcalc-smpos-cutadm} imply in particular that the sequent calculus gives us a posetal prop $\F\bSMPos\cG$.
  Moreover, the rules for $\tensor$ and $\one$ give $\F\bSMPos\cG$ the tensor and unit structure of \cref{thm:prop-tensor,thm:prop-unit}, so that it is a symmetric monoidal poset.
  Now if \cM is any other symmetric monoidal poset and $P:\cG\to\cM$ a map of symmetric relational polygraphs, there is a unique extension of $P$ to the objects of $\F\bSMPos\cG$.
  As usual, by induction on the rules of the sequent calculus and the fact that \cM is a posetal prop, this extension preserves the relations $\Gamma\le\Delta$.
  Finally, it also preserves the tensor and unit structure, so it is a strict functor of symmetric monoidal posets.
\end{proof}


\section{Props and symmetric monoidal categories}
\label{sec:prop-smc}

So much for symmetric monoidal posets.
What we really want, however, is a type theory for symmetric monoidal \emph{categories}, in which we can talk about equality of morphisms, and that can also deal with tensors in the codomain.

Unlike type theories for ordinary (symmetric) multicategories, even before we introduce any connectives we have a problem of non-uniqueness of derivations, because of the interchange rule.
A simple case is when we have $f\in \cG(A;B)$ and $g\in\cG(C;D)$; then there are two distinct derivations of a sequent for $f\circ_{()} g$:
\begin{mathpar}
  \inferrule*[Right=$g$]{
    \inferrule*{
      \inferrule*[Right=$f$]{
        \inferrule*{\inferrule*{ }{()\types()}}{A\types A}
      }{
        A\types B
      }}{
      A,C\types B,C
    }}{
    A,C\types B,D
  }\and
  \inferrule*[Right=$f$]{
    \inferrule*{
      \inferrule*[Right=$g$]{
        \inferrule*{\inferrule*{ }{()\types()}}{C\types C}
      }{
        C\types D
      }}{
      A,C\types A,D
    }}{
    A,C\types B,D
  }\and
\end{mathpar}
If we write down a term calculus whose terms correspond exactly to derivations, as we usually do, then the desired equality between these two derivations would look something like
\[ x:A, y:C \types (f,\idfunc)((\idfunc,g)(x,y)) \equiv (\idfunc,g)((f,\idfunc)(x,y)) : (B,D) \]
Note that unlike the $\beta$- and $\eta$-reductions, this equality is not directional: it makes no sense to regard one or the other side as ``simpler'' or ``more canonical'' than the other.
Thus, a canonical/atomic or focused theory will not help.

To deal with this in our type theory of props, we will break the bijection between terms and deductions, in a way that enables us to represent the above two derivations by \emph{literally the same} term (or tuple of terms), namely
\[ x:A, y:C \types (f(x),g(y)):(B,D) \]
This makes the metatheory and the initiality theorem rather more complicated, but at the end of the day it leads to a much more congenial type theory.

The intuition in this notation is of course that $f(x):B$ and $g(y):D$.
We could write it as ``$f(x):B,g(y):D$'', but we choose to tuple the terms up as in $(f(x),g(y)):(B,D)$ for a couple of reasons.
The first reason is that when doing equational reasoning, the equalities must relate entire tuples rather than single terms.
The second reason is that in general, we also need to include some ``terms without a type'' (e.g.\ coming from morphisms with empty codomain $()$, which is a judgmental representation of the unit object), and this looks a little nicer when all the terms are grouped together: we write for instance $(f(x),g(y)\mid h(z))$ to mean that $h(z):()$.

There are also, of course, function symbols with \emph{multiple} outputs.
To deal with this case we write $f_1(x)$, $f_2(x)$, and so on for the terms corresponding to all the types in the codomain.
For example, we write the composite of $f:(A,B) \to (C,D)$ with $g:(E,D)\to (F,G)$ as
\[ x:A, y:B, z:E \types (f_1(x,y),g_1(z,f_2(x,y)),g_2(z,f_2(x,y))):(C,F,G) \]
This does require one further technical device (that will be almost invisible in practice).
Suppose we have $f:()\to (B,C)$, written in type theory as $()\types (f_1,f_2):(B,C)$, and we compose/tensor it with itself to get a morphism $() \to (B,B,C,C)$.
We would na\"ively write this as $() \types (f_1,f_1,f_2,f_2)$, but this is ambiguous since we can't tell which $f_1$ matches which $f_2$.
We disambiguate the possibilities by writing $() \types (f_1,f'_1,f_2,f'_2)$ or $() \types (f_1,f'_1,f'_2,f_2)$.
Although this issue seems to only arise for morphisms with empty domain and greater than unary codomain, for consistency we formulate the syntax with a label (like $'$) on \emph{every} term former, and simply omit them informally when (as in the vast majority of cases) there is no risk of ambiguity.
We assume given an infinite alphabet of symbols \fA for this purpose (such as $','',''',\dots$, or $1,2,3,\dots$).

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$.
Note that the variables in a context are not literally treated ``linearly'', since they can occur multiple times in the multiple ``components'' of a map $f$.
For instance, a morphism $f:(A,B)\to (C,D)$ is represented by $x:A, y:B \types (f_1(x,y),f_2(x,y)):(C,D)$.
Instead the ``usages'' of a variable are controlled by the codomain arity of the morphisms applied to them.

\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:posetal-props}, 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\}} \pair{M}{N}^\fa \pc A\tensor B
    }\and
    \inferrule{\fL \finsubset \fA \\ \fa\notin\fL}{\Gamma\types^{\fL\cup\{\fa\}} \ttt^\fa\pc\unit}\and
    \inferrule{\Gamma\types^\fL M\pc A\tensor B \\ \fa\notin\fL}{\Gamma\types^{\fL\cup\{\fa\}} \pi_1^\fa(M) \pc A}\and
    \inferrule{\Gamma\types^\fL M\pc A\tensor B \\ \fa\notin\fL}{\Gamma\types^{\fL\cup\{\fa\}} \pi_2^\fa(M) \pc B}\and
    \inferrule{\Gamma\types^\fL M\pc \unit \\ \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},\pair{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},\pi_1^\fa(P),\pi_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,\ttt^\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}
  \pi_1^\fa(\pair M N^\fb) \equiv M\and
  \pi_2^\fa(\pair M N^\fb) \equiv N\and
  \pair{\pi_1^\fa(P)}{\pi_2^\fa(P)}^\fb \equiv P\and
  \cancel{\ttt^\fa}^\fb \equiv ()\and
\end{mathpar}
and also the following relation on lists:
\begin{mathpar}
  (\vec M,\ttt^\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 $\unit$ and prove the initiality theorem; there is very little difference with the prop case.
Similarly, we can construct ``presented'' props and symmetric monoidal categories by including arbitrary generators of $\equiv$.
In the next section we will use such equational theories to deduce some interesting results.

\section{Examples}
\label{sec:examples}

\subsection{Antipodes}
\label{sec:antipodes}

Recall that if $M$ is a bimonoid in a symmetric monoidal category, an \emph{antipode} is a map $i:M\to M$ such that
\begin{equation}
  \vcenter{\xymatrix@C=1pc{& M\otimes M \ar[rr]^{i\otimes 1} && M\otimes M \ar[dr]^m \\
      M \ar[ur]^{\Delta} \ar[dr]_{\Delta} \ar[rr]^{\varepsilon} && I \ar[rr]^{e} && M \\
      & M\otimes M \ar[rr]_{1\otimes i} && M\otimes M \ar[ur]_{m}}}
\end{equation}
commutes, where $\Delta$ and $\varepsilon$ are the comonoid structure of $M$.
A bimonoid equipped with an antipode is called a \emph{Hopf monoid} (or ``Hopf algebra'').
The question is whether an antipode for a bimonoid, if it exists, is unique?

In some cases we can apply cartesian reasoning.
For instance, the category of \emph{(co)commutative} comonoids in a symmetric monoidal category inherits a monoidal structure that turns out to be \emph{cartesian}, so a cocommutative bimonoid is actually a monoid in a cartesian monoidal category.
Similarly, the category of commutative monoids is cocartesian, so a commutative bimonoid is a comonoid in a cocartesian monoidal category, so we can apply the dual.
But what if neither the multiplication nor the comultiplication is commutative?

Using the type theory of props, we can describe monoids and comonoids in a roughly ``dual'' way, as follows.
Our generating polygraph \cG has one object $M$ and four morphisms
\begin{alignat*}{2}
m&:(M,M)\to M &&\quad\text{(written infix as $m(x,y) = x\cdot y$)}\\
e&:()\to M\\
\triangle&:M\to (M,M) &&\quad\text{(written a little abusively as $\triangle_i(x) = x_i$)}\\
\ep &:M\to () &&\quad\text{(written $\ep(x) = \cancel{x}$)}.
\end{alignat*}
The generators of the relation $\equiv$ are the axioms for a monoid and for a comonoid, written as follows:
\begin{alignat*}{2}
  x:M, y:M &\types x\cdot y:M &\qquad x:M &\types (x_1,x_2):(M,M)\\
  &\types e:M &\qquad x:M &\types (\mid\cancel{x}):()\\
  x:M,y:M,z:M &\types (x\cdot y)\cdot z = x\cdot (y\cdot z) :M &\qquad x:M &\types (x_{11},x_{12},x_2)=(x_1,x_{21},x_{22}):(M,M,M)\\
  x:M &\types x\cdot e=x:M &\qquad x:M &\types (x_1\mid\cancel{x_2}) = x:M\\
  x:M &\types e\cdot x=x:M &\qquad x:M &\types (x_2\mid\cancel{x_1}) = x:M
\end{alignat*}
plus the bimonoid axioms:
\begin{align*}
  x:M,y:M &\types (x_1\cdot y_1,x_2\cdot y_2) = ((x\cdot y)_1,(x\cdot y)_2) :(M,M)\\
          &\types (e_1,e_2)=(e,e):(M,M)\\
  x:M,y:M &\types (\mid\cancel{x\cdot y}) = (\mid\cancel{x},\cancel{y}) : ()\\
  &\types (\mid\cancel{e})=():()
\end{align*}
And an antipode is a map $x:M \types i(x):M$ such that
\begin{align*}
  x:M &\types x_1\cdot i(x_2) = (e\mid\cancel{x}) :M\\
  x:M &\types i(x_1)\cdot x_2 = (e\mid\cancel{x}) :M
\end{align*}
Now if we have another antipode $j$, we can compute
\begin{align*}
  x:M \types i(x)
  &= i(x)\cdot e\\
  &= (i(x_1)\cdot e\mid\cancel{x_2})\\
  &= i(x_1)\cdot (x_{21} \cdot j(x_{22}))\\
  &= (i(x_1)\cdot x_{21}) \cdot j(x_{22})\\
  &= (e \cdot j(x_{2})\mid\cancel{x_1})\\
  &= e\cdot j(x)\\
  &= j(x) \qquad :M
\end{align*}
yielding the same result $i=j$.
So even in a non-cartesian situation, we can use a very similar set-like argument, as long as we keep track of where elements get ``duplicated and discarded''.

\subsection{Duals and traces}
\label{sec:duals-traces}

If $A$ is an object of a prop, a \textbf{dual} of $A$ is an object $A^*$ with morphisms $\eta:()\to (A,A^*)$ and $\ep:(A^*,A)\to ()$ such that $\ep \circ_{A^*} \eta = \idfunc_A$ and $\ep \circ_{A} \eta = \idfunc_A^*$.
(In a symmetric monoidal category this reduces to the usual notion of dual.)
If $A$ has a dual $A^*$, and $f:A\to A$, the \textbf{trace} of $f$ is the composite 
\[ \tr(f) = \ep \circ_{A,A^*} (f \circ_A \eta) \]
or equivalently $(\ep \circ_A f)\circ_{A,A^*} \eta$.
In the type theory for props, the axioms of a dual say
\begin{mathpar}
  x:A \types (\eta_1 \mid \ep(\eta_2,x)) \equiv x :A\and
  y:A^* \types (\eta_2 \mid \ep(y,\eta_1)) \equiv y :A^*
\end{mathpar}
while the trace is $(\,\mid \ep(\eta_2,f(\eta_1)))$.
Recall that $\equiv$ is a congruence for substitution; thus the dual axioms mean that \emph{any term} $M$ (appearing even as a sub-term of some other term) can be replaced by $\eta_1^\fa$ if we simultaneously add $\ep^\fb(\eta_2^\fa,M)$ to the list of null terms (here \fa and \fb are fresh labels).
And dually, if $\ep^\fb(\eta_2^\fa,M)$ appears in the null terms, for any term $M$, then it can be removed by replacing $\eta_1^\fa$ (wherever it appears) with $M$.

Now a classical fact about the trace is that it is \emph{cyclic}: if $A$ and $A'$ both have duals $A^*$ and $(A')^*$, and $f:A\to A'$ and $g:A'\to A$, then $\tr(gf) = \tr(fg)$.
To prove this using traditional commutative-diagram reasoning is quite involved.
It does have a pretty and intuitive proof using string diagrams.
However, its proof in the type theory for props is one line:
\[ \tr(gf) = (\,\mid \ep(\eta_2,g(f(\eta_1))))
= (\,\mid \ep(\eta_2,g(\eta'_1)),\ep'(\eta'_2,f(\eta_1)))
= (\,\mid \ep(\eta'_2,f(g(\eta'_1))))
= \tr(fg).
\]
Here $\eta,\ep$ exhibit the dual of $A$, while $\eta',\ep'$ exhibit the dual of $A'$.
The first and last equality are by definition;
the second applies the first duality equation for $A'$ with $x=f(\eta_1)$; and the third applies the first duality equation for $A$ with $x=g(\eta'_1)$.

Note that these examples use only the type theory of props, not its extension to symmetric monoidal categories.
In general, because the underlying prop of a symmetric monoidal category remembers its morphisms both into and out of tensor products, it seems rarely necessary to invoke the actual tensor product objects.


\bibliographystyle{alpha}
\bibliography{all}

\end{document}