We give a natural-deduction-style type theory for symmetric monoidal categories whose judgmental structure directly represents morphisms with tensor products in their codomain as well as their domain.
The syntax is inspired by Sweedler notation for coalgebras, with variables associated to types in the domain and terms associated to types in the codomain, allowing types to be treated informally like “sets with elements” subject to global linearity-like restrictions.
We illustrate the usefulness of this type theory with various applications to duality, traces, Frobenius monoids, and (weak) Hopf monoids.

§ INTRODUCTION

§.§ Type theories for monoidal categories

Type theories are a powerful tool for reasoning about categorical structures.
This is best-known in the case of the internal language of a topos, which is a higher-order intuitionistic logic.
But there are also weaker type theories that correspond to less highly-structured categories, such as regular logic for regular categories, simply typed $\lambda$-calculus for cartesian closed categories, typed algebraic theories for categories with finite products, and so on (a good overview can be found in <cit.>).

However, type theories seem to be only rarely used to reason about non-cartesian monoidal categories.
Such categories are of course highly important in both pure mathematics and its applications (such as quantum mechanics, network theory, etc.), but usually they are studied using either traditional arrow-theoretic syntax or string diagram calculus [10, 21].

Type theories corresponding to non-cartesian monoidal categories do certainly exist — intuitionistic linear logic for closed symmetric monoidal categories, ordered logic for non-symmetric monoidal categories, classical linear logic for $\ast$-autonomous categories — but they are not widely used for reasoning about monoidal categories.
I believe this is largely because their convenience for practical category-theoretic arguments does not approach that of cartesian type theories.
The basic problem is that most nontrivial arguments in monoidal category theory involve tensor product objects in both the domain and the codomain of morphisms.

Existing type theories for non-cartesian monoidal categories fall into two groups, neither of which deals satisfactorily with this issue.
The first group is exemplified by intuitionistic linear logic, whose judgments have many variables as inputs but only a single term as output:

\[ x:A, y:B, z:C \types f(x,g(y,z)): D .\]

This allows the terms (such as $f(x,g(y,z))$) to intuitively “treat types as if they were sets with elements” (one of the big advantages of type-theoretic syntax).
But it privileges tensor products in the domain (here the domain is semantically $A\otimes B\otimes C$) over the codomain.
The only way to talk about morphisms into tensor products is to use the tensor product type constructor:

\[ x:A, y:B \types (y,x): B\otimes A. \]

This is asymmetric, but more importantly its term syntax is heavy and unintuitive: in the cartesian case we can use an element $p:A\times B$ by simply projecting out its components $\pi_1(p):A$ and $\pi_2(p):B$, but in the non-cartesian case we have to “match” it and bind both components as new variables:

\[ p:A\otimes B \types \flet (x,y) := p in (y,x) : B\otimes A. \]

The second group of non-cartesian type theories is exemplified by classical linear logic, whose judgments have multiple inputs as well as multiple outputs:

\[ A,B,C \types D,E. \]

This eliminates the asymmetry, but at the expense of no longer having a concise and intuitive term syntax.
Most commonly such type theories are presented as sequent calculi without any terms at all.
Term calculi do exist (e.g. [20, 4, 16, 6]) but usually involve some kind of “covariables”, losing the advantage of “treating types as sets with elements”.
Moreover, with only a few exceptions [22, 8], in type theories of this sort the tensor product appearing in codomains is usually a different one from the one appearing in domains (the “cotensor product” of a $\ast$-autonomous category), whereas in practical applications it happens very frequently that they are the same.

The purpose of this paper is to fill this gap, by describing a type theory for symmetric monoidal categories in which:

* Judgments have multiple inputs as well as multiple outputs.

* The tensor products appearing in domains and codomains are the same.

* There is a convenient and intuitive term syntax without the need for “covariables”, allowing us to resume “treating types as sets with elements”.
(In type-theoretic language, it is “natural deduction style” rather than “sequent calculus style”.)

* Tensor product types, though rarely needed, have a convenient term syntax involving “projections”, as in the cartesian case, rather than “matches”.

This type theory seems to be very convenient in practice for reasoning about symmetric monoidal categories.
We will show this in <ref> with a number of examples; here we sketch two of them to whet the reader's appetite.

For the first, recall that in a compact closed category, the trace $\tr(f)$ of an endomorphism $f:A\to A$ is the composite

\[ I \xto{\eta} A \otimes A^* \xto{f\otimes \id} A\otimes A^* \toiso A^* \otimes A \xto{\ep} I \]

where $I$ is the unit object, $A^*$ is the dual of $A$, and $\eta$ and $\ep$ are the unit and counit of the duality (also called the coevaluation and evaluation, respectively).
A fundamental property of the trace is that it is cyclic, i.e. $\tr(f g) = \tr(g f)$ for any $f:A\to B$ and $g:B\to A$.
The proof of this fact is essentially incomprehensible if written out in terms of composites of morphisms:

\begin{multline*}
\scriptstyle\tr(fg) = \ep \fs (fg \ten \id) \eta = \ep\fs(f\ten
\id)(g\ten \id)\eta =
\ep\fs(f\ten \id)(\id\ten\ep\ten\id)(\eta\ten\id\ten\id)(g\ten \id)\eta =\\
\scriptstyle\ep\fs(\id\ten\ep\ten\id)(f\ten
\id\ten\id\ten\id)(\id\ten\id\ten g\ten \id)(\eta\ten \eta) =
(\ep\ten\ep)\fs(\id\ten\id\ten g\ten \id)(f\ten \id\ten\id\ten\id)(\eta\ten \eta) =\\
\scriptstyle(\ep\ten\ep)\fs(\id\ten\id\ten g\ten
\id)(\id\ten\id\ten \eta)(f\ten \id)\eta =
\ep\fs(\id\ten\ep\ten\id)(g\ten\id\ten\id\ten\id)(\eta\ten\id\ten\id)(f\ten\id)\eta =\\
\scriptstyle\ep\fs(g\ten\id)(\id\ten\ep\ten\id)(\eta\ten\id\ten\id)(f\ten\id)\eta
= \ep\fs(g\ten\id)(f\ten\id)\eta = \ep\fs(gf\ten\id)\eta = \tr(gf).
\end{multline*}

It becomes much more understandable when written in string diagram calculus, as in <ref>.

[vert](f) at (0, -1)$f$;
[vert2](g) at (0, -3)$g$;

[->](g)to [out=-90, in =90] (.75, -5)to [out=-90, in =-90, looseness=2] (-.0,-5)
to [out=90, in =-90, looseness=1]
(.75,-3.25)–node[ed,swap, at end]$\rdual{A}$(.75, 0) to [out=90, in =90, looseness=2] (0, 0)–
node[ed,swap, at start]$A$(f);

[vert](f) at (0, -1)$f$;
[vert2](g) at (-1.5, -3)$g$;

[->](f)–node[ed]$B$(0, -2) to [out=-90, in =-90, looseness=2](-.75, -2) node[ed, right]$\rdual{B}$
to [out=90, in =90, looseness=2](-1.5,-2)–node[ed, swap, at start]$B$ (g);

[->](g)–node[ed, swap]$A$(-1.5, -3.5) to [out=-90, in =90](0, -5)to [out=-90, in =-90, looseness=2] (-.75,-5)
to [out=90, in =-90, looseness=1]
(.75,-3.5)–node[ed, swap, at end]$\rdual{A}$(.75, 0) to [out=90, in =90, looseness=2] (0, 0)–
node[ed, at start, swap]$A$(f);

[vert](f) at (0, -3)$f$;
[vert2](g) at (-1.5, -1)$g$;

[->](f) –node[ed, swap]$B$ (0, -3.5)  to [out=-90, in =-90, looseness=2](-.75, -3.5) –
node[ed, right, at end]$\rdual{B}$(-.75, 0)to [out=90, in =90, looseness=2](-1.5,0)–node[ed, swap, at start]$B$  (g);

[->](g)–node[ed, swap, near start]$A$(-1.5, -3.5)to [out=-90, in =90](0, -5)to [out=-90, in =-90, looseness=2] (-.75,-5)
to [out=90, in =-90, looseness=1](.75,-3.5)–node[ed, swap, at end]$\rdual{A}$(.75, -2) to [out=90, in =90, looseness=2] (0, -2)–
node[ed, at start, swap]$A$(f);

[vert](f) at (-3, -4)$f$;
[vert2](g) at (-1.5, -2)$g$;

[->](f) –node[ed, swap]$B$(-3, -5) to [out=-90, in =-90, looseness=2](-3.75, -5) –
(-3.75, -1.5) to[out=90, in =-90, looseness=.8]
node[ed, right, at end]$\rdual{B}$ (-2.25, 0)to [out=90, in =90, looseness=2](-3,0)to[out=-90, in =90, looseness=.8]
node[ed, swap, at start]$B$(-1.5, -1.5)– (g);

[->](g)–node[ed, near end]$A$(-1.5, -3)to [out=-90, in =-90, looseness=2] (-2.25,-3)
to [out=90, in =90]node[ed, swap, at end]$\rdual{A}$(-2.25, -3) to [out=90, in =90, looseness=2] (-3, -3)–
node[ed, at start, swap]$A$(f);

[vert](f) at (-1.5, -4)$f$;
[vert2](g) at (-1.5, -2)$g$;

[->](f) –(-1.5, -5) to [out=-90, in =-90, looseness=2](-2.25, -5) –
(-2.25, -1.5) to[out=90, in =-90, looseness=.8]
node[ed, right, at end]$\rdual{B}$ (-1.5, 0)to [out=90, in =90, looseness=2](-2.25,0)to[out=-90, in =90, looseness=.8]
node[ed, swap, at start]$B$(-1.5, -1.5)– (g);

Cyclicity of trace with string diagrams

But in our type theory, the proof is one line of algebra:

\begin{equation*}
\tr(f g) \defeq (\,\mid \eval{\abs{B} y}{fgy})
= (\,\mid \eval{\abs{B}{y}}{fx},\eval{\abs{A}{x}}{gx})
= (\,\mid \eval{\abs{A} x}{gfx})
\defeq \tr(g f).%\label{eq:intro-trace}
\end{equation*}

The reader is not expected to understand this proof yet, but to give some flavor we explain that the two non-definitional equalities are “$\beta$-reductions for duality”.
The binary operator $\eval{}{}$ denotes the counit $\ep$, while a variable/abstraction pair $(x,\abs{A}{x})$ denotes the unit $\eta$.
A term of the form $\eval{\abs{A}{x}}{t}$, where $x$ does not occur in $t$, is a $\beta$-redex for duality, and in the resulting reduction this term is eliminated and the occurrence of $x$ elsewhere[This “elsewhere” could be anywhere at all.
Thus although $\abs{A}{x}$ does “bind” the variable $x$, it does not delimit its scope.] is substituted by $t$.
(Semantically, this means applying a zigzag identity, which in string diagram calculus notation is “straightening a bent string”.)
Thus the middle term $(\,\mid \eval{\abs{B}{y}}{fx},\eval{\abs{A}{x}}{gx})$ contains two $\beta$-redexes, and the resulting two reductions yield the two terms on either side.

For our second example, recall that if $x$ is an element of a monoid $M$, and $\inv{x}$ and $\invt{x}$ are both two-sided inverses[In fact, of course, it suffices for $\inv{x}$ to be a left inverse and $\invt{x}$ a right inverse.] of $x$, then $\inv{x}=\invt{x}$ by the following calculation:

\begin{equation}
\inv{x} = \inv{x}e = \inv{x}(x\invt{x}) = (\inv{x}x)\invt{x} = e\invt{x} = \invt{x}.\label{eq:intro-classical-inversion}
\end{equation}

This same proof can be reproduced in cartesian type theory, and therefore holds for monoid objects in any cartesian monoidal category.
It follows that if a monoid object $M$ has an “inversion” morphism $i:M\to M$ such that

\begin{equation}\label{eq:intro-inversion}
\vcenter{\xymatrix@C=1pc{& M\times M \ar[rr]^{i\times 1} && M\times M \ar[dr]^m \\
M \ar[ur]^{\comult} \ar[dr]_{\comult} \ar[rr]^{!} && 1 \ar[rr]^{e} && M \\
& M\times M \ar[rr]_{1\times i} && M\times M \ar[ur]_{m}}}
\end{equation}

commutes (thereby making it a group object), then $i$ is the unique such morphism.

An interesting application of this relies on the fact that the category $\nCComon(\cC)$ of cocommutative comonoids in any symmetric monoidal category is in fact cartesian monoidal, with the cartesian product being the monoidal structure of .
A monoid object in $\nCComon(\cC)$ is a cocommutative bimonoid object in : an object with both a monoid and a cocommutative comonoid structure, such that the monoid structure maps are comonoid morphisms (or equivalently the comonoid structure maps are monoid morphisms).
For any bimonoid object, a morphism $i:M\to M$ satisfying the analogue of (<ref>):

\begin{equation}\label{eq:intro-antipode}
\vcenter{\xymatrix@C=1pc{& M\otimes M \ar[rr]^{i\otimes 1} && M\otimes M \ar[dr]^m \\
M \ar[ur]^{\comult} \ar[dr]_{\comult} \ar[rr]^{\varepsilon} && I \ar[rr]^{e} && M \\
& M\otimes M \ar[rr]_{1\otimes i} && M\otimes M \ar[ur]_{m}}}
\end{equation}

(where $\comult,\varepsilon$ are the comonoid structure) is called an antipode, and a bimonoid object equipped with an antipode is called a Hopf monoid.
Thus, the classical argument for uniqueness of inverses, phrased in cartesian type theory, implies that a cocommutative bimonoid object has at most one antipode.
Dualizing, we can conclude that a commutative bimonoid object also has at most one antipode.

For bimonoids that are neither commutative nor cocommutative, cartesian type theory cannot help us.
We can manually translate the classical proof (<ref>) into commutative diagrams and then replace all the $\times$'s by $\otimes$'s, but this is tedious and one feels that there should be a better way.
And indeed, in our type theory for symmetric monoidal categories, we can write a very close analogue of (<ref>) that applies to arbitrary bimonoids:

\begin{equation}
\inv{x} = \inv{x}\,e = (\inv{x\s1}\, e \mid \cancel{x\s2}) = \inv{x\s1}\, x\s2 \,\invt{x\s3} = (e\, \invt{x\s2} \mid \cancel{x\s1}) = e\,\invt{x} = \invt{x}.
\label{eq:intro-antipode-uniq}
\end{equation}

Again, the reader is not expected to understand this completely, but the resemblance to (<ref>) should be clear.
The main differences are the subscripts on the $x$'s and the insertion of the steps $(\inv{x\s1}\, e \mid \cancel{x\s2})$ and $(e\, \invt{x\s2} \mid \cancel{x\s1})$.
The subscripts are used to track applications of the comultiplication $\comult:M\to M\otimes M$.
This is necessary because (unlike in the cartesian case) not all morphisms are comonoid morphisms (so that $f(x)\s1$ might differ from $f(x\s1)$), and also because in the absence of cocommutativity the resulting “copies” of $x$ must be distinguished (so that $(x\s1,x\s2)$ is different from $(x\s2,x\s1)$).
Similarly, the canceled terms such as $\cancel{x\s2}$ track applications of the counit $\ep : M\to I$, and the steps involving these are inserted in order to match the middle composite $M\xto{\ep} I \xto{e} M$ in (<ref>).

With this as preview and motivation, we now move on to a somewhat more detailed description of our type theory.

§.§ Generalized Sweedler notation

The idea behind our type theory is to formalize and generalize the informal Sweedler notation that is common in coalgebra theory.
A coalgebra is a comonoid in the category of vector spaces, i.e. a vector space $C$ with a comultiplication $\comult : C\to C\otimes C$ that is coassociative and counital.
Since the elements of the tensor product $C\otimes C$ are finite sums of generating tensors $c\s1 \otimes c\s2$, we can write

\[ \comult(c) = \sum_i c^i\s1 \otimes c^i\s2. \]

Sweedler's notation is to omit the index $i$, and sometimes also the summation symbol $\sum$, obtaining

\[ \comult(c) = c\s1 \otimes c\s2. \]

(This is therefore a sort of “dual” to the “Einstein summation convention” for products of tensors, which also has a type-theoretic formalization known to physicists as “abstract index notation” [17].)
For instance, coassociativity can then be expressed as

\[ c\s1 \otimes c\ss21 \otimes c\ss22 = c\ss11 \otimes c\ss12 \otimes c\s2 \]

(which is then often written as $c\s1 \otimes c\s2 \otimes c\s3$),
and counitality, for a counit $\ep$, can be expressed as

\[ c\s1 \cdot \ep(c\s2) = c = \ep(c\s1) \cdot c\s2 \]

where $\cdot$ denotes scalar multiplication.

We generalize this notation to apply to any morphism $f:A \to B\otimes C$ in any monoidal category whose codomain is a tensor product.
Of course we now have to notate which morphism we are talking about, so instead of $c\s1\otimes c\s2$ we write $f\s1(x) \otimes f\s2(x) : B\otimes C$, where $x:A$ is a formal variable.

Note that in Sweedler's original notation for coalgebras in vector spaces, the element $\comult(c)$ really is a sum of generating tensors $c\s1 \otimes c\s2$, whereas now we are in an arbitrary monoidal category so that this doesn't even make sense.
Nevertheless, we can still use a similar formal notation governed by appropriate rules, just as in type theory we use variables and terms assigned to objects of the category as “types” even though the objects of an arbitrary category may not actually have “elements”.

However, as a nod towards this extra formality (and also an extra step in the “types are like sets” direction),

we stop using the symbol $\otimes$ and write instead a pair $(f\s1(x), f\s2(x)):(B,C)$.
We also have to incorporate an analogue of “scalar multiplication”, which in a general monoidal category means the unit isomorphism $C\otimes I \cong C$; for consistency we collect all the “scalars” in a separate tuple separated by a bar.
Thus, for instance, the counitality of a comultiplication $\comult : C\to C\otimes C$ with counit $\ep : C\to I$ in an arbitrary monoidal category will be expressed as

\[ (\comult\s1(c) \mid \ep(\comult\s2(c))) = c = (\comult\s2(c) \mid \ep(\comult\s1(c))). \]

Similarly, the composite of $f:A \otimes B \to C\otimes D$ with $g:E\otimes D\to F\otimes G$ along the object $D$ is

\[
\inferrule{x:A, y:B \types (f\s1(x,y),f\s2(x,y)):(C,D) \\ z:E,w:D \types (g\s1(z,w),g\s2(z,w):(F,G)) }
{x:A, y:B, z:E \types (f\s1(x,y),g\s1(z,f\s2(x,y)),g\s2(z,f\s2(x,y))):(C,F,G)}
\]

Note that in contrast to intuitionistic linear logic, the variables in a context are not literally treated “linearly” in our terms, since they can occur multiple times in the multiple “components” of a map $f$.
Instead, the “usages” of a variable are controlled by the codomain arity of the morphisms applied to them.

One further technical device is required to deal with morphisms having nullary domain.
Suppose we have $f:I\to B\otimes C$, written in our type theory as $\types (f\s1,f\s2):(B,C)$, and we compose/tensor it with itself (and apply a symmetry) to get a morphism $I \to B\otimes B\otimes C\otimes C$.
We would naïvely write this as $ \types (f\s1,f\s1,f\s2,f\s2) : (B,B,C,C)$, but this is ambiguous since we can't tell which $f\s1$ matches which $f\s2$.
Thus, we disambiguate the possibilities by annotating the terms in pairs, such as $() \types (f\s1,f'\s1,f\s2,f'\s2)$ or $() \types (f\s1,f'\s1,f'\s2,f\s2)$.

The “variable-binding notation” $(x,\abs{A}{x})$ for duality that we mentioned earlier is just syntactic sugar for a special case of this: we use variables like $x$ as the “labels” for unit morphisms $\eta_A : () \to (A,A^*)$ in place of primes, writing $(x,\abs{A}{x})$ instead of $((\eta_A)^x\s1,(\eta_A)^x\s2)$.
Of course, this requires that the “variables” used as labels of this sort are disjoint from those occurring in the actual context.
The operator $\eval{}{}$ is just an infix notation for the counit $\ep:(A^*,A)\to ()$.

Another bit of syntactic sugar is that if each type is equipped with at most one specified comonoid structure, then there is no ambiguity in reverting back to Sweedler's original notation $(x\s1,x\s2)$ instead of $(\comult\s1(x),\comult\s2(x))$.
For instance, the axiom of a Frobenius algebra can be written as

\[ (x\s1, x\s2 y) = ((xy)\s1,(xy)\s2) = (x y\s1, y\s2) \]

while the principal axiom of a bialgebra is

\[ ((xy)\s1,(xy)\s2) = (x\s1 y\s1, x\s2 y\s2). \]

Note that if all types have such a comonoid structure and all morphisms are comonoid morphisms, which in type-theoretic notation means $f(x)\s{i} = f(x\s{i})$ and $\ep(f(x)) = \ep(x)$, then the monoidal structure automatically becomes cartesian.
In ordinary type theory for cartesian monoidal categories, the diagonal (i.e. the comultiplication) is represented by literally duplicating a variable $(x,x)$; thus our subscripting of variables $(x\s1,x\s2)$ can be viewed as a minimal modification of this to deal with situations where the comultiplication is not literally a cartesian diagonal.
(Indeed, the comultiplication of a coalgebra is often viewed as a non-cartesian substitute for the diagonal, e.g. in the theory of quantum groups.)
We can similarly regard the counit $\ep$ as a “discarding” operation, in which case I like to notate $\ep(x)$ by $\cancel{x}$ (as was done in (<ref>)).

§.§ Type theory versus string diagrams

String diagrams (a.k.a. graphical calculus) are another well-known and very powerful tool for working with structures in many kinds of monoidal categories.
Like any tool, they have both strengths and weaknesses.
String diagrams are at their best when dealing with structures whose axioms “don't change the topology”, such as dual pairs and Frobenius algebras, since in this case many proofs are simply topological deformations.
For structures whose axioms do change the topology, such as bialgebras and Hopf algebras, string diagrams are still useful, but in such cases only some of the proof steps can be reduced to simple topological deformations: generally those steps involving pure naturality conditions.

I view the type theory presented here as complementary to string diagrams, with different strengths and weaknesses.
It does not “see” the topological nature of structures such as dual pairs and Frobenius algebras, so in such situations string diagrams may be preferable.
However, it represents most naturality conditions as syntactic identities, making them completely invisible; for instance, the two middle steps in <ref> disappear entirely in (<ref>).
Moreover, it leverages a different intuition, allowing us to think of objects of an arbitrary monoidal category as “sets” with “elements” (modulo certain “linearity” restrictions).
This is particularly useful for coalgebraic and Hopf-type structures — perhaps unsurprisingly, given the origin of our syntax in Sweedler notation.

Another difference is that string diagrams incarnate categorical duality in an obvious way — by simply rotating or reflecting a string diagram — while our type theory breaks this duality, treating inputs and outputs differently.
One might consider this an advantage of string diagrams.
But breaking duality in the syntax is part of what gives us the above advantages (notably the view of types as sets), and it also means that duality becomes a nontrivial and useful technique: in a situation that is not self-dual, we can choose which orientation of the type theory is most convenient.
For instance, in <ref> we will use our type theory to show that the antipode of a (weak) Hopf monoid is a monoid anti-homomorphism; it then follows by duality that it is also a comonoid anti-homomorphism, although a direct proof of the latter in our syntax would be less intuitive.

Only time and experience can render a final verdict on the usefulness of a notation.
This includes particularly an exploration of its generalizations and limitations, e.g. does the type theory presented in this paper admit generalizations to other kinds of monoidal categories, such as closed, $\ast$-autonomous, braided, ribbon, and planar monoidal categories, indexed monoidal categories,
(symmetric) monoidal bicategories,
and so on?
My primary hope for this paper is to begin a conversation about all such type theories and their potential uses.

§.§ Acknowledgements

I would like to thank Dan Licata, Robin Cockett, and Peter LeFanu Lumsdaine for useful conversations.

§ PROPS

To simplify and clarify the semantics of our type theory, rather than interpreting it directly in symmetric monoidal categories, we will interpret it in a categorical structure that reflects the type-theoretic distinction between judgmental and type operations.
To explain what this means, recall that ordinary cartesian type theory is often interpreted in categories with finite products; but in this case both the judgmental comma (in a context $(x:A, y:B, z:C)$) and the product type operation (in a product type $(A\times B)\times C$) are interpreted by the same categorical operation (cartesian product types), which can cause confusion.
A more direct semantics of cartesian type theory maintains this distinction by using a “cartesian multicategory”, allowing the judgmental comma to be interpreted by the “categorical comma”, i.e. the concatenation that forms a list of objects to be the domain of a morphism in a multicategory.

For type theories like classical linear logic, which allow multiple types in both domain and codomain but use commas on the left and right of the turnstile to represent different tensor products, the appropriate “multicategorical” structure is called a “polycategory” [23] (the corresponding “monoidal” version being a linearly distributive [7, 4] or $\ast$-autonomous [1, 2] category).
In our case, where the two tensor products are the same, the appropriate structure is called a prop.

A prop $\cP$ consists of

* A set $\ob(\cP)$ of objects, and

* A symmetric strict monoidal category (that is, a symmetric monoidal category whose associators and unitors are identities) whose underlying monoid of objects is freely generated by $\ob(\cP)$.

(The original Adams–MacLane [14] definition of prop had only one object; thus our “props” are sometimes called “colored props”.)

We write the objects of the monoidal category in <ref> as finite lists $(A,B,\dots,Z)$ of objects of the prop (i.e. $A,B,\dots,Z\in\ob(\cP)$).
The monoidal structure is given by concatenation of lists; the unit object is the empty list $()$.

We now summarize the relationship between props and symmetric monoidal categories.

A tensor product $A\otimes B$ of objects in a prop is an object together with an isomorphism

\[ (A,B) \toiso (A\otimes B) \]

in the monoidal category of <ref><ref>.
Similarly, a unit is an object $I$ with an isomorphism

\[ () \toiso (I) .\]

A prop is called representable if it has a unit and any pair of objects has a tensor product.

A morphism of props $\omega : \cP\to\cQ$ is a function $\omega_0 : \ob(\cP) \to \ob(\cQ)$ together with a strict symmetric monoidal functor whose action on objects is obtained by applying $\omega_0$ elementwise to lists.

The category of symmetric monoidal categories and strong symmetric monoidal functors is equivalent to the subcategory of representable props (and all morphisms between them).

Every symmetric monoidal category has an underlying prop $U\cC$ with the same objects, and in which a morphism $(A,\dots,B) \to (C,\dots, D)$ is a morphism $A\otimes \cdots \otimes B \to C\otimes\cdots \otimes D$ in .
This construction $U$ is functorial on strong symmetric monoidal functors, and the props in its image are representable.
(In fact, it is the functorial strictification.)
The functor $U$ is faithful since the action of $f:\cC\to\cD$ on objects and arrows is preserved in $U f$, while the coherence constraints of $f$ are recorded in the action of $U f$ on the isomorphisms from <ref>.
Similarly, the functor $U$ is full, since the action of a morphism $U \cC\to U\cD$ on the isomorphisms from <ref> induces symmetric monoidal constraints on its underlying ordinary functor.
Finally, every representable prop induces (by choosing tensor products and a unit) a symmetric monoidal structure on its category of unary and co-unary morphisms, and it is isomorphic to the underlying prop thereof.

We can say more: this subcategory is an injectivity-class, and the corresponding category of algebraic injectives (objects equipped with chosen lifts against the generating morphisms, and maps that preserve the chosen lifts) is equivalent to the category of symmetric monoidal categories and strict symmetric monoidal functors.
In particular, the latter is monadic over the category of props.

The fundamental “initiality theorem” for semantics of our type theory, which we prove in <ref>, is that the “term model” is the prop freely generated by some input data.
Following [3], we will call this input data a signature.

A signature is a set of objects together with a set of arrows, each assigned a domain and codomain that are both finite lists of objects.

The category of props is monadic over the category of signatures.

Just like the proof in <cit.> for the one-object case.

Thus, every prop has a presentation as a coequalizer of a pair of maps between free props.
In <ref> we will extend our type theory to construct “presented props” as well, allowing equational reasoning as in the examples from <ref>.

The fact that props allow multiple objects in both domains and codomains means that we rarely need to talk about actual tensor product types $A\otimes B$ with semantics in tensor product objects (<ref>).
For this reason, we will not include such types in our formal system.
However, we note that if necessary, they can be added quite easily: because <ref> simply asserts objects, morphisms, and equations (rather than a unique factorization property), it can essentially be ensured as a special case of a prop presentation.
Thus we need only add some generating terms and axioms to our type theory, for any pair of objects $A,B$ whose tensor product we need to talk about:

x:A, y:B xy:A⊗Bp : A⊗B (π1(p), π2(p)) : (A,B) (x,y) = (π1x y, π2x y)p = π1(p)π2(p).

Note how similar this is to the treatment of cartesian products in cartesian type theory with pairing and projection operations.

§ ON THE ADMISSIBILITY OF STRUCTURAL RULES

In general, type theories consist of rules for deriving judgments about terms.
The most common judgments are typing judgments (that a term belongs to a type, or in our case a tuple of terms belong to a tuple of types) and equality judgments (that two terms — or tuples of terms — are equal).
A tree of rules ending with a judgment is called a derivation of that judgment, and the categorical structure presented by a type theory is built out of the derivable (or valid) judgments.

Now in proving that this categorical structure does in fact have the desired universal property, it is very useful if we arrange the type theory so that every derivable judgment has a unique derivation.
The reason for this is that we want a morphism in our categorical semantics to be determined by a term itself, not by a choice of derivation of that term; but the natural way to prove the desired universal property (a.k.a. the “initiality theorem” for that type theory) is by induction over derivations.
Thus, if the same term can arise from multiple derivations, proving this universal property requires an extra step of proving that this choice is immaterial (i.e. that any two derivations of the same term determine the same morphism in the semantics).
This step is tricky and often omitted in the literature, leading to incomplete proofs.
It becomes even trickier when considering higher-categorical semantics, in which the morphisms determined by two derivations of the same term may be only isomorphic rather than equal.

The choice that terms should have unique derivations essentially requires that nearly all structural rules should be admissible rather than primitive.
(Recall that an admissible rule is one that is not asserted as part of the specification of the type theory, but for which we can prove after the fact that whenever we have derivations of its premises we can construct a derivation of its conclusion — usually by inductively traversing and modifying the given derivations of its premises.
The structural rules are, roughly speaking, those that correspond to the operations of the categorical structure used as the semantics: composition in a category, permutation of domain lists in a symmetric multicategory, and permutation of both domains and codomains in a polycategory or prop.)

The reason this requirement arises is that structural rules generally have to satisfy equations that are “tautological” in their action on terms.
For instance, composing $f:A\to B$ with $g:B\to C$ and $h:C\to D$ in the two possible ways (semantically, $h\circ (g\circ f)$ and $(h\circ g)\circ f$) produces the same term:

*x:A f(x): B
y:B g(y):Cx:A g(f(x)):C
z:C h(z):D
x:A h(g(f(x))) :D*x:A f(x): B

*y:B g(y):C
z:C h(z):Dy:B h(g(y)):D
x:A h(g(f(x))) :D
Thus, if composition were a primitive rule, this term would have two distinct derivations.
But if composition (i.e. substitution) is an admissible rule, then we can prove that the derivations constructed by applying it in these two different ways turn out to be the same.
Similarly, if permutation were primitive, then for any $f:(A,B) \to C$ we would have two (in fact, infinitely many) derivations of the same term:

x:A ,y:B f(x,y):C  x:A ,y:B f(x,y):Cy:B,x:A f(x,y) :C x:A ,y:B f(x,y):C

whereas if permutation (a.k.a. “exchange”) is admissible, then its functoriality as an operation on derivations can be proven.

Type theorists know how to make a rule admissible: we build “just enough” of it into the primitive rules.
For instance, if we introduce generating morphisms such as $f:(A,B) \to C$ and $g:C\to D$ as simple axioms (i.e. rules with no premises):

x:A, y:B f(x,y):C z:C g(z):D

then there would be no way to construct derivations of composites such as

\begin{equation}
\inferrule{x:A, y:B \types f(x,y):C \\ z:C \types g(z):D}{x:A, y:B \types g(f(x,y)) : D}\label{eq:primcomp}
\end{equation}

except by using a primitive composition/substitution rule.
Therefore, we instead introduce each generating morphism in “Yoneda style” by allowing ourselves to postcompose any given term(s) with it.
For instance, in cartesian type theory we introduce generators with rules such as

for arbitrary contexts $\Gamma$ and terms $a,b,c$.
Now (<ref>) can be obtained without a primitive substitution rule:

\begin{equation}
\inferrule*{\inferrule*{\inferrule*{ }{x:A,y:B \types x:A}\\
\inferrule*{ }{x:A,y:B \types y:B}}
{x:A,y:B \types f(x,y):C}}
{x:A,y:B \types g(f(x,y)):D}\label{eq:admcomp}
\end{equation}

In categorical terms, the point is that we can build the free category on a graph either by freely adding all binary (and nullary) composites and then quotienting by the relation of associativity, or we can avoid the need to quotient at all by defining the morphisms as composable lists of generating arrows, where a “list” is defined inductively as either an empty list or a list postcomposed by a generating arrow — that is, we enforce right-associated composites $k\circ (h\circ (g\circ (f\circ \id)))$.

This technique is trickier in non-cartesian type theories, since we cannot keep the same context all the way through the derivation.
That is, in a cartesian monoidal category we can start (<ref>) with the “identity” or “axiom” rules $x:A,y:B \types x:A$ and $x:A,y:B \types y:B$, corresponding categorically to the projections $A\times B\to A$ and $A\times B\to B$; but in a non-cartesian monoidal category such projections do not exist.
Thus, we need to concatenate contexts as we go down the derivation tree.
For instance, the generator rule for $f:(A,B)\to C$ must be something like

\begin{equation}
\inferrule{\Gamma\types a:A \\ \Delta\types b:B}{\Gamma,\Delta \types f(a,b):C}.\label{eq:gen1}
\end{equation}

However, now we have a new problem: the exchange rule (permutations of the domain).
In the cartesian case, we can make this admissible by “propagating it up” the entire derivation since the context remains the same.
For instance, if we permute the inputs of (<ref>) we would simply get

\begin{equation}
\inferrule*{\inferrule*{\inferrule*{ }{y:B,x:A \types x:A}\\
\inferrule*{ }{y:B,x:A \types y:B}}
{y:B,x:A \types f(x,y):C}}
{y:B,x:A \types g(f(x,y)):D}\label{eq:permcomp}
\end{equation}

But in the non-cartesian case this doesn't work.
We don't want to assert a primitive exchange rule as this would break the “terms have unique derivations” principle, so instead we build exchange into the generator rule (<ref>).
Our first try might be something like

\[
\inferrule{\Gamma\types a:A \\ \Delta\types b:B \\ \si:\Gamma,\Delta \cong \Phi}{\Phi \types f(a,b):C}
\]

where $\si$ is an arbitrary permutation.
But this too breaks the “terms have unique derivations” principle, since a permutation of types within $\Gamma$ or $\Delta$ could be obtained either as part of $\si$ or by operating on the input derivations of $\Gamma\types a:A$ and $\Delta\types b:B$.
Instead we have to build in “just enough” exchange but not too much, by requiring $\si$ to be not an arbitrary permutation but a shuffle: a permutation of $(\Gamma,\Delta)$ that preserves the relative order of the types in $\Gamma$ and in $\Delta$.
We will write $\nShuf(\Gamma;\Delta)$ for the set of such shuffles.

This may seem overly technical, but the presence of such things as shuffles need never be seen by the user of the type theory.
Indeed, maintaining the “terms have unique derivations” principle is precisely what allows the user to work only with terms, ignoring the details of the derivations.

§ THE TYPE THEORY FOR FREE PROPS

Let be a signature; we will define a type theory that presents the free prop on .
Our general typing judgment will be of the form shown in <ref>.
For reasons to be explained later, we annotate some of the types in the consequent of each judgment with a superscript star, $\actv{B}$, and call them active; we write $\maybeactv{B}$ to mean that $B$ might be active.

\begin{align*}
x_1:A_1, \dots ,x_m:A_m &\types (M_1,\dots,M_n \mid Y_1,\dots, Y_p) :(\maybeactv{B_1},\dots,\maybeactv{B_n}).\\
x_1:A_1, \dots ,x_m:A_m &\types (M_1,\dots,M_n \mid Y_1,\dots, Y_p) = (N_1,\dots,N_n \mid Z_1,\dots, Z_q) :(B_1,\dots,B_n).
\end{align*}

\begin{align*}
\Gamma &\types (\vec{M} \mid \vec{Y}) :\maybeactv{\vec{B}}.\\
\Gamma &\types (\vec{M} \mid \vec{Y}) = (\vec{N} \mid \vec{Z}) :\vec{B}.
\end{align*}

Judgments, abbreviated

We use vector notation $\vec{M},\vec{A},$ etc. to indicate a list of terms or types, so the judgments can be abbreviated as in <ref>, although this omits the information that $\vec{M}$ and $\vec{N}$ must have the same length as $\vec{B}$ (while the length of $\vec{Y}$ and $\vec{Z}$ is unrestricted).
If $\vec{Y}$ is empty, we write $(\vec{M}\mid )$ as simply $(\vec{M})$.
If furthermore $\vec{M}$ and $\vec{B}$ have length 1, we omit the parentheses, writing simply $M : B$.
When all the lists are empty, we have $\types () : ()$, which will be valid (it represents the identity morphism of the unit object).

In these judgments $A_i,B_j$ are types, $x_i$ are variables, and $M_j,N_j,Y_k,Z_\ell$ are terms.
Here by a type we simply mean an object of our generating signature $\cG$, since there are no type-forming operations in the theory.
There is nothing new in our variables; the reader who prefers de Bruijn indices is free to think of them in that way, although since our syntax has no variable binding[Recall that in the notation $(x,\abs{A} x)$ for the unit of a duality, $x$ is not actually a variable in this sense but rather one of the labels $\fA$.] the usual subtleties of capture-avoidance are irrelevant.

The terms are defined inductively by the rules shown in <ref>.
Note that they are “well-scoped” by definition: they come with a context and only use variables occurring in that context.
We subscript only applications of functions with greater than unary codomain, and as noted in <ref>, we annotate each occurrence of a morphism with nullary domain and positive-ary codomain with some element of an infinite alphabet of symbols (such as $','',''',\dots$, or $1,2,3,\dots$).

(x:A) ∈ΓΓx f∈(;B_1,…,B_n)

n ≥2
1≤k ≤n
Γf^k f∈(;B)

Γf ΓM_1

f∈(A_1,…,A_m; B_1,…, B_n)

n ≥2
1 ≤k ≤n
Γfk(M_1,…,M_m) ΓM_1

f∈(A_1,…,A_m; B_1,…, B_n)

n ≤1

We will write $\vec{f}(\vec{M})$ for the list of all subscriptings of the application of $f$ to the arguments $\vec{M}$.
That is, for $f\in \cG(A_1,\dots,A_m;B_1,\dots,B_n)$ we have

\[
\vec{f}(\vec{M}) =
\begin{cases}
(f^\fa\s1 ,\dots, f^\fa\s n) &\qquad m=0,\, n\ge 2\\
f^\fa &\qquad m=0,\, n= 1\\
f &\qquad m=0,\, n= 0\\
(f\s1(\vec{M}),\dots,f\s n(\vec{M})) &\qquad m\ge 1,\, n\ge 2\\
f(\vec{M}) &\qquad m\ge 1,\, n\le 1
\end{cases}
\]

In the first and second case, we also write $\vec{f}^\fa$ to notate the label .
In the third case, we allow ourselves to write $\vec{f}^\fa$ to mean simply $f$ (discarding the label).
Finally, when $n\le 1$ we allow ourselves to write $f\s1$ or $f\s1(\vec{M})$ to mean $f$ or $f(\vec{M})$ respectively.

We define the “simultaneous substitution” of a list of terms $\vec M$ for a list of variables $\vec x$ in the usual way, as shown in <ref>.

x_k[M_1,…,M_n/x_1,…,x_n]    = M_k

y[M⃗/x⃗]    = y      (y∉x⃗)

f^k[M⃗/x⃗]    = f^k

f^[M⃗/x⃗]    = f^

f[M⃗/x⃗]    = f

fk(N,…,P)[M⃗/x⃗]    = fk(N[M⃗/x⃗],…,P[M⃗/x⃗])

f(N,…,P)[M⃗/x⃗]    = f(N[M⃗/x⃗],…,P[M⃗/x⃗])

Simultaneous substitution into terms

We now move on to the rules governing our typing judgment.
In <ref> we argued that by incorporating Yoneda-style generator rules and shuffles, we can make composition and exchange admissible and thereby ensure that any judgment has a unique derivation.
In the case of props, we also want to make the monoidal structure admissible (since it satisfies strict associativity and interchange laws that we would otherwise have to assert as judgmental equalities).
In particular, for morphisms $f:A\to B$ and $g:C\to D$ we would like the judgment

\[ x:A , y:C \types (f(x), g(y)) : (B,D) \]

to have a unique derivation.
Symmetry suggests that this unique derivation cannot apply $f$ first and then $g$ or vice versa.
Thus, we replace the generator rule by a “multi-generator” rule allowing only a one-step derivation

\[ \inferrule{x:A,y:C \types (x,y):(A,C)}{x:A,y:C \types (f(x),g(y)):(B,D)} \]

In general, if $f$ is a morphism in , we write $\vec f(\vec M)$ for the list of “all the values of $f$” applied to the list of arguments $\vec M$.
Thus if $f:(A,B,C)\to (D,E)$ then $\vec f(\vec M)$ would be $(f\s1(M_1,M_2,M_3),f\s2(M_1,M_2,M_3))$.

Thus, a first approximation to our multi-generator rule is

\[ \inferrule*{
\Gamma \types (\vec M,\dots,\vec N,\vec P \mid \vec Z)
: (\vec A,\dots, \vec B,\vec C)\\
f \in \cG(\vec A,\vec D)\\\cdots\\
g \in \cG(\vec B,\vec E)
}{\Gamma \types (\vec f(\vec M),\dots,\vec g(\vec N),\vec P \mid \vec Z)
: (\vec D,\dots, \vec E,\vec C)}
\]

However, if there are generators with nullary codomain, we need to collect them into the scalar terms $\vec Z$.
Thus a second approximation is

\[ \inferrule*{
\Gamma \types (\vec M,\dots,\vec N,\vec P,\dots,\vec Q,\vec R \mid \vec Z)
: (\vec A,\dots, \vec B,\vec C,\dots,\vec D, \vec E)\\
f \in \cG(\vec A,\atleastone{\vec F})\\\cdots\\
g \in \cG(\vec B,\atleastone{\vec G})\\\\
h \in \cG(\vec C,())\\\cdots\\
k \in \cG(\vec D,())
}{\Gamma \types
\left(\vec f(\vec M),\dots,\vec g(\vec N),\vec R
\;\middle|\;
h(\vec P),\dots, k(\vec Q), \vec Z\right)
: (\vec F,\dots, \vec G,\vec E)}
\]

(Here $\atleastone{\vec F}$ means that $\vec F$ contains at least one type.)
Eventually we will also incorporate shuffles, but we postpone that for now.
Let us consider instead how to prevent duplication of derivations.
In addition to our desired term

\begin{align}
x:A, y:C &\types (f(x),g(y)):(B,D)\label{eq:prop-good-term}
\intertext{we must also be able to write}
x:A, y:C &\types (f(x),y):(B,C)\label{eq:prop-goodish-term-1}\\
\intertext{and}
x:A, y:C &\types (x,g(y)):(A,D)
\end{align}

so how do we prevent ourselves from being able to apply the generator rule again to the latter two, obtaining two more derivations of the same morphism as (<ref>)?
The idea is to force ourselves to “apply all functions as soon as possible”: we cannot apply $g$ to $y$ in (<ref>) because we could have already applied it to produce (<ref>).
On the other hand, we could apply $h:(B,C) \to E$ in (<ref>) to get

\[ x:A, y:C \types (h(f(x),y)):E \]

because $h$ uses $f$ as one of its inputs and so could not have been applied at the same time as $f$.

Making this precise is the purpose of designating some of the types in the consequent as active; recall that we denote the active types by $\actv{A}$.
If $\vec{A}$ is a list of types, we write $\oneactv{\vec A}$ to mean that at least one of the types in $\vec A$ is active, $\allactv{\vec A}$ to mean that they are all active, and $\zeroactv{\vec A}$ to mean that none of them are active.
We write $\maybeactv{\vec A}$ to avoid specifying whether or not any of the types are active.

The identity rule will make all types active, while the generator rule makes only the outputs of the generators active.
We then restrict the generator rule to require that at least one of the inputs of each generator being applied must be active in the premise; this means that none of them could have been applied any sooner, since at least one of their arguments was just introduced by the previous rule.
Thus, our desired derivation

** x:A,y:C (x,y):(A,C)x:A,y:C(f(x),g(x)):(B,D)

is allowed, while the undesired one

\begin{equation*}
\text{\textquestiondown} \qquad \inferrule*{\inferrule*{\inferrule*{ }{x:A,y:C \types (x,y):(\actv{A},\actv{C})}}{x:A,y:C\types (f(x),y):(\actv{B},C)}}{x:A,y:C \types (f(x),g(y)):(B,D)} \qquad ?
\end{equation*}

is not allowed, since in the attempted application of $g$ the input type $C$ is not active.
Thus our generator rule now becomes

\[ \inferrule*{
\Gamma \types (\vec M,\dots,\vec N,\vec P,\dots,\vec Q,\vec R \mid \vec Z)
: (\oneactv{\vec A},\dots, \oneactv{\vec B},\oneactv{\vec C},\dots,\oneactv{\vec D}, \maybeactv{\vec E})\\
f \in \cG(\vec A,\atleastone{\vec F})\\\cdots\\
g \in \cG(\vec B,\atleastone{\vec G})\\\\
h \in \cG(\vec C,())\\\cdots\\
k \in \cG(\vec D,())
}{\Gamma \types
\left(\vec f(\vec M),\dots,\vec g(\vec N),\vec R
\;\middle|\;
\vec h(\vec P),\dots,\vec k(\vec Q), \vec Z\right)
: (\allactv{\vec F},\dots, \allactv{\vec G},\zeroactv{\vec E})}
\]

Of course, this rule can now never apply to generators with nullary domain.
Since these can always be applied at the very beginning, we incorporate them into the identity rule.
Thus the identity rule is now

\[\inferrule{
f \in \cG((),\atleastone{\vec{B}})\\\cdots\\
g \in \cG((),\atleastone{\vec{C}})\\\\
h \in \cG((),())\\\cdots\\
k \in \cG((),())\\\\
\fa,\dots,\fb\in \fA\text{ and pairwise distinct}
}{\vec x:\vec A\types
\left(\vec x,{\vec f}^{\fa},\dots,{\vec g}^{\fb} \,\middle|\, h,\dots,k\right)
:(\allactv{\vec A}, \allactv{\vec B}, \dots,\allactv{\vec C})}
\]

Note that we include labels on the terms with nullary domain and positive-ary codomain, as promised.

Finally, if we want to make the exchange rule admissible, we have to build permutations into the rules as well.
Each rule should add exactly the part of a permutation that can't be “pushed into the premises”.
Because we've formulated the generator rule so that the premise and conclusion have the same context, any desired permutation in the domain can be pushed all the way up to the identity rule.
Thus, for the generator rule it remains to deal with permutation in the codomain.

The freedom we have in the premises of the generator rule is to (inductively) permute the types within each list $\vec A,\vec B,\vec C,\vec D,\vec E$, and also to block-permute the lists $\vec A,\dots,\vec B$ and separately the lists $\vec C,\dots,\vec D$ (with a corresponding permutation of the generators $f,\dots,g$ and $h,\dots,k$).
(If we permuted the main premise any more than this, it would no longer have the requisite shape to apply the rule to.)
Permutations of $\vec C,\dots,\vec D$ don't do us any good in terms of permuting the codomain of the conclusion, but we can push permutations of $\vec E$ directly into the premise, and also a block-permutation of $\vec F,\dots,\vec G$ into a block-permutation of $\vec A,\dots,\vec B$.

What remains that we have to build into the rule can be described precisely by a permutation of $\vec F,\dots,\vec G,\vec E$ that (1) preserves the relative order of the types in $\vec E$, and (2) preserves the relative order of the first types $F_1,\dots,G_1$ in the lists $\vec F,\dots,\vec G$.
That is, any permutation of $\vec F,\dots,\vec G,\vec E$ can be factored uniquely as one with these two properties followed by a block sum of a block-permutation of $\vec F,\dots,\vec G$ with a permutation of $\vec E$.
(The choice of the first types is arbitrary; we could just as well use the last types, etc.)

There is no real need to allow ourselves to permute the scalar terms, since semantically their order doesn't matter anyway.
But it is convenient to allow ourselves to write the scalar terms in any order, so we incorporate permutations there too.
The freedom in the premises allows us to permute the term in $\vec Z$ arbitrarily, and also to permute the terms $h,\dots,k$ among themselves; thus what remains is precisely a shuffle.
The final generator rule is therefore the first rule shown in <ref>.

Γ(M⃗,…,N⃗,P⃗,…,Q⃗,R⃗ |Z⃗)
: (A⃗,…, B⃗,C⃗,…,D⃗, E⃗)

f ∈(A⃗,F⃗)

g ∈(B⃗,G⃗)

h ∈(C⃗,())

k ∈(D⃗,())

σ: (F⃗,…, G⃗,E⃗) Δ preserving activeness

σ preserves the relative order of types in  E⃗

σ preserves the relative order of  F_1,…, G_1

Γ( σ(f⃗(M⃗),…,g⃗(N⃗),R⃗)
τ(h(P⃗),…,k(Q⃗), Z⃗))
: Δ

f ∈((),B⃗)

g ∈((),C⃗)

h ∈((),())

k ∈((),())

,…,∈ and pairwise distinct

σ: (A⃗, B⃗, …,C⃗) Δ preserving activeness

σ preserves the relative order of  B_1,…, C_1
x⃗:A⃗(σ(x⃗,f⃗^,…,g⃗^ )  |  h,…,k)

Rules of the typing judgment

In the identity rule, the only useful freedom in the premises is to block-permute the $\vec B,\dots,\vec C$.
Thus what remains is a permutation that preserves the relative order of the first types $B_1,\dots, C_1$.
Any permutation in the scalar terms can be pushed into the premises, so we have the final rule shown second in <ref>.
Note that this also allows us to incorporate an arbitrary permutation in the domain.

Having introduced the auxiliary notion of “active types” to ensure that typing judgments have unique derivations, we now proceed to eliminate it.
We start with the following observation.
The notion of subterm is defined as usual; we write $M\equiv N$ to mean that $M$ and $N$ are syntactically the same term.

If $\Gamma \types (\vec M\mid\vec Z):\Delta$ is derivable, and some $M_i$ is a subterm of some $M_j$, then $i=j$ (hence $M_i\equiv M_j$).

By induction on the derivation.
In an application of the identity rule, the non-scalar terms have no subterms, so the assumption means that $M_i\equiv M_j$.
And since these terms are also uniquely identified by their label, we have $i=j$.

For an application of the generator rule, all the non-scalar terms either occur verbatim in the main premise, xor are of the form $f\s k(\vec M)$ (including $f(\vec{M})$ when $k=1$) where each $M_i$ is a non-scalar term in the main premise and $|\vec{M}|\ge 1$.
Let us call these old and new terms respectively.

The inductive hypothesis takes care of the case when both terms are old.
If a new term $f\s k(\vec M)$ is a subterm of an old term $N$, then each $M_i$ is a proper subterm of $N$, contradicting the inductive hypothesis.
Similarly, if an old term $N$ is a proper subterm of a new term $f\s k(\vec M)$, then it must be a subterm of some $M_i$, also contradicting the inductive hypothesis.

If one new term $f\s k(\vec M)$ is a proper subterm of another $g\s \ell(\vec N)$, then it must be a subterm of some $N_j$.
Hence each $M_i$ must be a proper subterm of $N_j$, contradicting the inductive hypothesis.

Finally, suppose two new terms are syntactically equal, $f\s k(\vec M) \equiv g\s \ell(\vec N)$.
Then we must have $f=g$, $k=\ell$, and $\vec M \equiv \vec N$.
Note that $f=g$ means that $f$ and $g$ are the same function symbol (morphism in ), but not a priori that they arise from the same generator application in the rule.
However, $\vec M \equiv \vec N$ and the inductive hypothesis ensure that this is in fact the case.
Together with $k=\ell$, this implies that they have the same place in the given judgment as well.

Semantically, it is not really necessary to label the morphisms in $\cG(;B)$ with a symbol $\fa\in\fA$, since tensor products of such morphisms are invariant under permutation (because the swap on the unit object is the identity morphism).
However, it would be significantly trickier to omit such labels syntactically.
In practice, we can leave them off informally and trust the reader to put them back if needed.

If there is some assignment of activeness to the types in $\Delta$ such that $\Gamma \types (\vec M\mid\vec Z):\Delta$ is derivable, then that assignment is unique, as is the derivation.

By the depth of an occurrence of a variable or function symbol in a term, we mean the rank of its corresponding node in the well-founded abstract syntax tree representing the term.
Thus the depth of a variable is $0$, and the depth of an occurrence of a function symbol is the least natural number strictly greater than the depths of the head symbols of all its arguments.

Note that a nullary function symbol always has depth $0$, while a function symbol applied to a positive number of variables alone has depth $1$.

We claim that in any derivable typing judgment, the terms associated to active types are precisely those non-scalar ones whose head symbol has maximum depth.
The proof is by induction on derivations.
In the identity rule, all terms have depth $0$ and all types are active.
Now consider the generator rule, and suppose inductively that the claim is true for the main premise, with maximal depth $n$, say.
Then since each of the new function symbols introduced by the rule is applied to at least one term from an active type, which therefore has the maximal depth $n$, it must have depth $n+1$.
It follows that the new maximum depth is $n+1$, and that these new symbols are precisely those of maximum depth; but they are also precisely those associated to active types.
This proves the claim.

It follows immediately that the terms uniquely determine the activeness of the types, since depth is a syntactic invariant of the terms.
Moreover, we can tell from the terms which rule must have been applied last (if the maximum depth is $0$, it must come from the identity rule; otherwise it must come from the generator rule) and which function symbols that rule must have introduced (those of maximum depth).

In the case of the generator rule, we also have to group the new terms into applications $\vec f(\vec M)$ of a list of function symbols.
This is not trivial since a given function symbol could be applied twice by the same generator rule; but by <ref> we can tell whether two terms resulted from the same application by checking whether their arguments are syntactically equal.
Now the ordering of these function symbol applications as $f,\dots,g$ and $h,\dots,k$ must be the order in which the corresponding $f\s1,\dots,g\s1$ and $h,\dots,k$ appear in the term list, since the permutations $\sigma$ and $\tau$ preserve those orders.
Then $\sigma^{-1}$ is uniquely determined by the fact that it must place all the outputs of $f$ first, and so on until all the outputs of $g$, then all the terms of non-maximum depth in the same order that they were given in the conclusion.
Similarly, $\tau^{-1}$ is uniquely determined by the fact that it has to place $h,\dots,k$ first and the scalar terms of non-maximum depth last, preserving internal order in each group.
Finally, this determines the main premise uniquely as well.

The argument for the identity rule is similar, with no $\tau$ and with $\sigma^{-1}$ placing all the variables first in the order of the context.
Inductively, therefore, the entire derivation is uniquely determined.

Note that we can regard this proof as an algorithm for “type-checking” a judgment without activeness annotations: first we use the recursive depth function on terms to calculate the activeness, then we proceed as usual to recursively match against the generator or identity rules.
Because of this theorem, in the future we will omit the activeness labels.

Γ(M⃗ |Z_1,…,Z_n) : Δ
: ≅Γ(M⃗ |Z_1,…,Z_n) = (M⃗^|Z^_ρ1,…,Z^_ρn) : Δ

Rule of the axiom-free equality judgment

It remains to consider the equality judgment.
We don't have a traditional form of $\alpha$-conversion since we have no bound variables as such, but as remarked in <ref> the labels $\fa\in\fA$ can sometimes be regarded as playing a similar role, and in particular the choice of concrete labels must not matter.
We also need to impose invariance under permutation of the scalar terms.
It may seem silly to have incorporated permutations in the scalar terms earlier and yet quotient out by that freedom now, but such an equality rule would be necessary even if we hadn't incorporated any permutations to start with.
The paradigmatic case is when we have two nullary scalar generators $f:() \to ()$ and $g:()\to ()$, leading unavoidably to two distinct valid terms

( |f,g) :( |g,f) :
that must be equal in a monoidal category (since the monoid of endomorphisms of the unit object is commutative).
It is probably no coincidence that this is also the case where interesting things happen upon categorification.

Combining these two permutation rules, we obtain the rule shown in <ref>.
When we consider presented props in <ref>, with equational theories, we will need the usual reflexivity, symmetry, transitivity, and congruence rules for equality, but with only this rule we can omit them since permutations are already a group.
And since we have no type forming operations, there are no $\beta$ or $\eta$ rules.

This completes our definition of the type theory for the free prop generated by .

§ CONSTRUCTING FREE PROPS FROM TYPE THEORY

We now proceed to show that our type theory has the structure of a prop, beginning with the admissibility of exchange on the right.

If $\Gamma\types (\vec{M}\mid\vec{Z}) : \Delta$ is derivable and $\rho$ is a permutation of $\Delta$, then  $\Gamma\types (\rho\vec{M}\mid\vec{Z}) : \rho\Delta$ is also derivable.
Moreover, this action is functorial.

This essentially follows from how we built the rules.
If the derivation ends with the identity rule, then we can compose $\rho$ with the specified permutation $\sigma$ from that rule, and reorder the generators $f,\dots,g$ in the rule according to the order that $\rho\sigma$ puts them in.
If the derivation ends with the generator rule, then we similarly compose $\rho$ with $\sigma$, reorder the generators $f,\dots,g$, and inductively push the remaining part of the permutation (that acting on the non-active terms) into the main premise.
Functoriality follows immediately.

For admissibility of composition/substitution, it seems helpful to first prove the admissibility of a single-generator rule.
Note that we formulate it with the domain of the generator at the end of the given codomain context.

If $\Gamma\types (\vec{M},\vec{N}\mid \vec{Z}): \Delta,\vec A$ is derivable and $f\in \cG(\vec A,\vec B)$, then $\Gamma\types (\vec{M},\vec{f}(\vec{N})\mid \vec{Z}): \Delta,\vec B$ is derivable.
Moreover, if none of the types in $\vec A$ are active in the given derivation, then all of the types in $\Delta$ that are active in the given derivation are still active in the result.

If any of the types in $\vec A$ are active, we can simply apply the generator rule with $f$ as the only generator.
Otherwise, none of them were introduced by the final rule in the given derivation.
If that final rule was the identity rule, then $\vec A$ must be empty (since all types in the conclusion of the identity rule are active), so $f$ has nullary domain and we can just add it to that application of the identity rule.

If the final rule in the given derivation was the generator rule, then $\vec A$ must also appear at the end of its main premise.
If none of the types in $\vec A$ are active therein, then we can inductively apply $f$ to that premise; by the second clause of the inductive hypothesis, this does not alter the activeness of the other types in the premise, so we can re-apply the generator rule.
Finally, if at least one of the types in $\vec A$ is active in the main premise, then we can add $f$ to the generator rule, applying it alongside all the other generators, since it satisfies the condition that at least one of its arguments be active.
(Technically, this may require us to first permute the consequent of the main premise so that $\vec A$ appears before all the other non-inputs to the generator rule.
This is not a problem for the induction since in this case we are not actually using the inductive hypothesis at all.)
In all cases, the second claim of the lemma is obvious.

Now by combining <ref>, we can postcompose with a generator $f\in \cG(\vec A,\vec B)$ whose domain types $\vec A$ appear anywhere in the consequent of a judgment $\Gamma\types (\vec{M}\mid\vec{Z}):\Delta$, in any order.

Substitution is admissible: if $\Gamma\types (\vec{M}\mid\vec{Y}) : \Delta$ and $\Delta \types (\vec{N}\mid\vec{Z}) : \Phi$ are derivable, then so is $\Gamma\types (\vec{N}[\vec{M}/\Delta] \mid \vec{Z}[\vec{M}/\Delta],\vec{Y}) : \Phi$.

We induct on the derivation of $\Delta \types (\vec{N}\mid\vec{Z}) : \Phi$.
If it comes from the identity rule, then we just have to compose $\Gamma\types (\vec{M}\mid\vec{Y}) : \Delta$ with some number of nullary-domain generators and permute its codomain; we do this one by one using <ref> and then <ref>.
Similarly, if it comes from the generator rule, we inductively compose with its main premise, then apply all of the new generators one by one using <ref>.

As an example, suppose we want to compose the following terms:

\begin{gather}
x:A,y:B \types (f\s1(y),k(g,f\s3(y)),f\s2(y) \mid h(x)) : (C,D,E)\label{eq:ceg5a}
\\\notag\\
u:C,v:D,w:E \types (m(u,\ell\s2(w)),s,\ell\s1(w) \mid n(v)) : (F,G,H)\label{eq:ceg5b}
\end{gather}

Here the generators are

f:B →(C,E,P)g:() →Qh:A →()k:(Q,P) →Dℓ:E →(H,R)m:(C,R) →Fn:D→()s:() →G

The depths are

f=1g=0h=1 k=2ℓ=1 m=2 n=1 s=0

Thus, the final rule of the second derivation must apply $m$ only, so our inductive job is to compose

\begin{gather}
x:A,y:B \types (f\s1(y),k(g,f\s3(y)),f\s2(y) \mid h(x)) : (C,D,E)\label{eq:ceg2a}
\\\notag\\
u:C,v:D,w:E \types (u,\ell\s2(w),s,\ell\s1(w) \mid n(v)) : (C,R,G,H)\label{eq:ceg2b}
\end{gather}

Now the final rule of the second derivation must apply $\ell$ and $n$ together, so our inductive job is to compose

\begin{gather}
x:A,y:B \types (f\s1(y),k(g,f\s3(y)),f\s2(y) \mid h(x)) : (C,D,E)\label{eq:ceg1a}
\\\notag\\
u:C,v:D,w:E \types (w,v,u,s \mid\,) : (E,D,C,G)\label{eq:ceg1b}
\end{gather}

The latter is obtained from the identity rule, so our task is now to apply <ref> to the former and the single generator $s:()\to G$.
Peeling down the derivation of the former, we obtain

\[ x:A,y:B \types (g,f\s3(y),f\s1(y),f\s2(y) \mid h(x)) : (Q,P,C,E) \]

and then

\[ x:A,y:B \types (y,x,g \mid\,) : (B,A,Q) \]

which is also obtained from the identity rule.
The identity rule can therefore also give us

\[ x:A,y:B \types (y,x,g,s \mid\,) : (B,A,Q,G). \]

Re-applying $f,h$ and then $k$, we obtain

\[ x:A,y:B \types (g,f\s3(y),f\s1(y),f\s2(y),s \mid h(x)) : (Q,P,C,E,G) \]

and then

\[ x:A,y:B \types (f\s1(y),k(g,f\s3(y)),f\s2(y),s \mid h(x)) : (C,D,E,G). \]

Permuting this, we obtain

\[ x:A,y:B \types (f\s2(y),f\s1(y),k(g,f\s3(y)),s \mid h(x)) : (E,C,D,G). \]

as the result of composing (<ref>) and (<ref>).

Backing out the induction one more step, we must apply $\ell$ and $n$ to this using <ref>.
We cannot apply $\ell$ directly since its domain $E$ is not active (its term $f\s2(y)$ has depth $1$ while the maximum depth is $2$).
Thus, we back up to the main premise

\[ x:A,y:B \types (g,f\s3(y),f\s1(y),f\s2(y),s \mid h(x)) : (Q,P,C,E,G) \]

in which $E$ is active.
Thus, we can apply $\ell$ in the same generator rule as $k$, obtaining

\begin{multline}
x:A,y:B \types (\ell\s1(f\s2(y)),\ell\s2(f\s2(y)),f\s1(y),k(g,f\s3(y)),s \mid h(x))\\ : (H,R,C,D,G).\label{eq:ceg4}
\end{multline}

Now the domain $D$ of the generator $n$ is active, so we can directly apply it with another generator rule, obtaining (after permutation)

\begin{multline}
x:A,y:B \types (f\s1(y),\ell\s2(f\s2(y)),s,\ell\s1(f\s2(y)) \mid n(k(g,f\s3(y))),h(x))\\ : (C,R,G,H).\label{eq:ceg3}
\end{multline}

as the result of composing (<ref>) and (<ref>).

Finally, we must compose this with $m$ using <ref>.
Neither of the domain types $C$ and $R$ is active in (<ref>) (in fact, no types are active in (<ref>), since the last rule applied was a generator rule whose only generator has nullary codomain), so we have to inductively peel back to (<ref>) in which $R$ is active (though not $C$).
Thus, we can then apply $m$ in the same generator rule as $n$, obtaining

\begin{multline}
x:A,y:B \types (m(f\s1(y),\ell\s2(f\s2(y))),s,\ell\s1(f\s2(y)) \mid n(k(g,f\s3(y))),h(x))\\ : (F,G,H)\label{eq:ceg}
\end{multline}

as our end result.

Note that the terms in (<ref>) are indeed the result of substituting $f\s1(y)$ for $u$, $k(g,f\s3(y))$ for $v$, and $f\s2(y)$ for $w$ (the terms appearing in (<ref>)) in the terms of (<ref>), and appending the scalar term $h(x)$ of (<ref>) to the scalar terms of (<ref>):

\begin{align*}
m(u,\ell\s2(w))[f\s1(y)/u, k(g(f\s3(y)))/v, f\s2(y)/w]
&= m(f\s1(y),\ell\s2(f\s2(y)))\\
s[f\s1(y)/u, k(g(f\s3(y)))/v, f\s2(y)/w]
&= s \\
\ell\s1(w)[f\s1(y)/u, k(g(f\s3(y)))/v, f\s2(y)/w]
&= \ell\s1(f\s2(y))\\
n(v)[f\s1(y)/u, k(g(f\s3(y)))/v, f\s2(y)/w]
&= n(k(g(f\s3(y)))).
\end{align*}

The only choice involved in the proof of <ref> is in how to order the scalar terms in the result.
We adopted the convention that those associated to the terms being substituted into come first, followed by those associated to the terms being substituted.
The opposite convention would do as well for the following theorem:

Composition is associative and unital.

Since derivations are determined uniquely by their terms by <ref>, this follows from the evident associativity and unitality of substitution into terms, and the associativity and unitality of concatenation of lists of scalar terms.

Thus we have a category whose objects are contexts and whose morphisms are derivable judgments $\Gamma\types (\vec{M}\mid\vec{Z}) : \Delta$.
However, this is not quite the underlying category of our prop: we must quotient it by the equality rule from <ref>:

\begin{equation}\label{eq:prop-perm-2}
\inferrule{\Gamma\types (\vec M \mid Z_1,\dots,Z_n) : \Delta \\ \rho \in S_n \\ \si : \fA \cong \fA}{\Gamma\types (\vec M \mid Z_1,\dots,Z_n) = (\vec M^\si \mid Z^\si_{\rho 1},\dots,Z^\si_{\rho n}) : \Delta}
\end{equation}

(which also ensures that the choice of ordering in <ref> is irrelevant).
For this we need the evident observation:

The equality rule (<ref>) is a congruence on the category of contexts and derivable typing judgments.
That is, it is an equivalence relation on the morphisms that is preserved by composition on both sides.

Therefore, the quotient by this equality judgment is again a category whose objects are the contexts (i.e. finite lists of types).

The contexts and derivable term judgments in the type theory for the free prop generated by , modulo the equality rule (<ref>), form a symmetric strict monoidal category.

The monoidal structure on contexts is concatenation, with the empty context as unit.
To tensor morphisms, it is easiest to first tensor with identities: given $\Gamma\types (\vec M\mid \vec Z):\Delta$, we construct $\Gamma,\vec x:\vec A\types (\vec M,\vec x\mid \vec Z):\Delta,\vec A$ by inducting until we get down to the identity rule and then adding the variables $\vec{x}:\vec{A}$ to the context.
Now we obtain the tensor product of $\Gamma\types (\vec{M}\mid\vec{Y}) : \Delta$ and $\Phi\types (\vec{N}\mid \vec{Z}): \Psi$ by first tensoring with identities to get $\Gamma,\Phi \types (\vec{M},\Gamma \mid\vec{Y}): \Delta,\Phi$ and $\Delta,\Phi\types (\Delta,\vec{N}\mid\vec{Z}) : \Delta,\Psi$ and then composing to get $\Gamma,\Phi\types (\vec{M},\vec{N}\mid \vec{Z},\vec{Y}) : \Delta,\Psi$.
If we did this in the other order, we would get $(\vec{M},\vec{N}\mid \vec{Y},\vec{Z})$ instead, which is equal by (<ref>).
In particular, this implies functoriality of the tensor product; associativity and unitality follow similarly.
Finally, the symmetry isomorphism is $\vec x:\vec A, \vec y:\vec B \types (\vec y,\vec x) : \vec B,\vec A$; it is easy to verify the axioms.

Thus we have a prop, which we denote $\F{}\cG$.

$\F{}\cG$ is the free prop generated by .

Let be a prop and $\pfree:\cG\to \cP$ a morphism of signatures.
We extend it to a morphism of props $\F{}\cG \to \cP$ by induction on derivations.
By the coherence theorem for symmetric monoidal categories (e.g. <cit.>), there is a unique choice at each step if we are to have a (symmetric strict monoidal) functor, and likewise both equality rules corresponds to actual equalities that must hold in .
Then we prove that this actually is a symmetric strict monoidal functor, using the definition of composition and the tensor product in $\F{}\cG$.

Since the free prop generated by a signature is unique up to isomorphism, it follows that our $\F{}\cG$ is isomorphic to the free prop on presented in any other way, such by using string diagrams whose edges and vertices are labeled by objects and morphisms of respectively.
Unsurprisingly, this correspondence can be made more explicit: from any derivable $\Gamma \types \vec M : \Delta$ we can construct a labeled string diagrams from $\Gamma$ to $\Delta$, whose vertices are the generator applications and whose edges are the disjoint union of the variables in $\Gamma$ and the terms $f\s i(\vec N)$ appearing as subterms of $\vec M$.

§ PRESENTATIONS OF PROPS

Since the category of props is monadic over the category of signatures by <ref>, every prop has a presentation in terms of signatures, i.e. a coequalizer diagram

\[ \F{}\cR \toto \F{}\cG \to \cP. \]

Moreover, since $\F{}$ and its right adjoint are the identity on the set of objects, we may assume that $\cR$ and $\cG$ both have the same set of objects as and all the morphisms are the identity on objects.
Now by the universal property of $\F{}\cR$, the two morphisms of props $\F{}\cR \toto \F{}\cG$ are equivalently morphisms of signatures $\cR \toto \F{}\cG$.
Thus, once $\cG$ is given, the additional data of $\cR$ consists of a set of pairs of parallel morphisms in $\F{}\cG$, which is to say a set of equality axioms of the form

\[ \Gamma \types (\vec{M}\mid\vec{Y}) = (\vec{N} \mid\vec{Z}) : \Delta \]

where both $\Gamma \types (\vec{M}\mid\vec{Y}) : \Delta$ and $\Gamma\types (\vec{N} \mid\vec{Z}):\Delta$ are derivable in the type theory for the free prop generated by .
We obtain the type theory for the prop presented by $(\cG,\cR)$ by augmenting the type theory for the free prop on by these axioms for the equality judgment, together with the additional rules shown in <ref> (which are no longer automatic in the presence of such axioms).

Γ(M⃗|Z⃗) : ΔΓ(M⃗|Z⃗) = (M⃗|Z⃗) : Δ
Γ(M⃗|Y⃗) = (N⃗ |Z⃗) : ΔΓ(N⃗ |Z⃗) = (M⃗|Y⃗) : Δ
Γ(M⃗|X⃗) = (N⃗ |Y⃗) : Δ

Γ(N⃗ |Y⃗)  = (P⃗|Z⃗) : Δ
Γ(M⃗|X⃗) = (P⃗ |Z⃗) : Δ
Γ(M⃗|X⃗) = (N⃗ |Y⃗) : Δ

Δ(P⃗ |Z⃗) : Φ
Γ(P⃗[M⃗/Δ] |Z⃗[M⃗/Δ], X⃗) =
(P⃗[N⃗/Δ] |Z⃗[N⃗/Δ], Y⃗) : Φ
Γ(M⃗|X⃗) : Δ

Δ(N⃗ |Y⃗) = (P⃗ |Z⃗) : Φ
Γ(N⃗[M⃗/Δ] |Y⃗[M⃗/Δ], X⃗) =
(P⃗[M⃗/Δ] |Z⃗[M⃗/Δ], X⃗) : Φ
Γ(M⃗|X⃗) = (N⃗ |Y⃗) : Δ

Φ(P⃗|Z⃗) = (Q⃗ |W⃗) : Ψ
Γ,Φ(M⃗,P⃗ |X⃗, Z⃗) = (N⃗, Q⃗ |Y⃗,W⃗) : Δ,Ψ

Γ(M⃗ |Z_1,…,Z_n) : Δ
: ≅Γ(M⃗ |Z_1,…,Z_n) = (M⃗^|Z^_ρ1,…,Z^_ρn) : Δ

Rules of the equality judgment in the presence of axioms

The first three rules in <ref> are the usual reflexivity,[Actually, it is not necessary to assert reflexivity explicitly, since it is a special case of the permutation rule.] symmetry, and transitivity.
The next three are congruence rules for precomposition, postcomposition, and the concatenation product.
The final one is the label-renaming and scalar-permutation rule from <ref>.
Note that congruence for pre- and post-composition includes congruence under permutations of the domain and codomain.

For any prop presentation $(\cG,\cR)$, the equality judgment generated by the axioms of together with the rules of <ref> is a congruence on the prop $\F{}\cG$.
That is, it is an equivalence relation on morphisms preserved by composition and tensor product.

The rules of <ref> essentially force this to be true.

Thus we obtain a prop $\F{}\langle\cG|\cR\rangle$ as the quotient of $\F{}\cG$ by this congruence.

$\F{}\langle\cG|\cR\rangle$ is the prop presented by $(\cG,\cR)$.
That is, we have a coequalizer diagram in the category of props:

\[ \F{}\cR \toto \F{}\cG \to \F{}\langle\cG|\cR\rangle. \]

Since the quotient map $\F{}\cG \to \F{}\langle\cG|\cR\rangle$ is surjective, a prop morphism $\pfree:\F{}\cG \to \cP$ factors through $\F{}\langle\cG|\cR\rangle$ in at most one way.
Moreover, it does so precisely when it identifies all pairs of tuples of terms that are identified by the equality judgment.
However, the equality rules in <ref> are satisfied in any prop, so this happens precisely when $\pfree$ respects the axioms of , i.e. when it coequalizes the two maps $\F{}\cR \toto \F{}\cG$.

Thus, we can use our type theory to reason about structures in arbitrary props defined by generators and axioms, and hence also in symmetric monoidal categories (by <ref>).

§ EXAMPLES

§.§ Duals and traces

We begin by repeating the first example from the introduction more carefully.
The free prop generated by a dual pair has a generating signature $\cG$ with two objects $A$ and $A^*$ and two morphisms $\eta:()\to (A,A^*)$ and $\ep:(A^*,A)\to ()$, and a signature of relations that imposes two axioms

x:A (η1 |(η2,x)) = x :Ay:A^* (η2 |(y,η1)) = y :A^*.

A map from this prop to a symmetric monoidal category then reduces to the usual notion of dual.

As suggested in the introduction, we write $\eval{M}{N}$ for $\ep(M,N)$, and $(u,\abs{A} u) : (A,A^*)$ for $(\eta\s1,\eta\s2)$, where $u$ is a label (i.e. an element of $\fA$) rather than a variable (appearing in the context).
In this notation, the axioms are

x:A (u |Aux) = x :Ay:A^* (A u |yu) = y :A^*.

Recall that $=$ is a congruence for substitution on both sides.
Thus the first axiom means that if $\eval{\abs{A}u}{M}$ appears in the scalars, for any term $M:A$ not involving $u$, then it can be removed by replacing $u$ (wherever it appears, even as a subterm of some other term) with $M$.
This justifies regarding it as a sort of “$\beta$-reduction for duality” with $u$ playing the role of a “bound variable”, although as we noted in the introduction the “binder” $\abs{A} u$ does not delimit the “scope” of $u$ at all.
Running this rule in reverse, we see that any term $M:A$ (appearing even as a sub-term of some other term) can be replaced by $u$, for a fresh label $u$, if we simultaneously add $\eval{\abs{A}u}{M}$ to the scalars.
The other axiom is similar; we may regard it as an “$\eta$-reduction for duality”.

If $A$ has a dual $A^*$, and $f:A\to A$, the trace of $f$ is the composite

\[ () \xto{\eta} (A,A^*) \xto{(f,\idfunc)} (A,A^*) \xto{\cong} (A^*,A) \xto{\ep} () \]

In our type theory this is

\[ () \types (\,\mid \eval{\abs{A} u}{f(u)}) : ().\]

As advertised in the introduction, we can now prove cyclicity of the trace with a $\beta$-expansion followed by a $\beta$-reduction: for morphisms $f:A\to B$ and $g:B\to A$, with $A$ and $B$ dualizable, we have

\begin{align*}
\tr(f g) &\defeq (\,\mid \eval{\abs{B} y}{f(g(y))})\\
&= (\,\mid \eval{\abs{B}{y}}{f(x)},\eval{\abs{A}{x}}{g(x)})\\
&= (\,\mid \eval{\abs{A} x}{g(f(x))})\\
&\defeq \tr(g f).
\end{align*}

More generally, any $f:(Y,A) \to (Z,A)$ has a “partial” or “twisted” trace

\[ y:Y \types (f\s1(y,u) \mid \eval{\abs{A}u }{f\s2(y,u)} ) : Z.  \]

This satisfies a version of cyclicity <cit.>: for any morphisms $f:(Y,A) \to (Z,B)$ and $g:(W,B) \to (X,A)$, with $A$ and $B$ dualizable, we have

\begin{align*}
y:Y, w:W &\types (g\s1(w,v), f\s1(y,g\s2(w,v)) \mid \eval{\abs{B} v}{f\s2(y,g\s2(w,v))}) \\
&= (g\s1(w,v), f\s1(y,u) \mid \eval{\abs{B} v}{f\s2(y,u)}, \eval{\abs{A} u}{g\s2(w,v)})\\
&= (g\s1(w,f\s2(y,u)), f\s1(y,u) \mid \eval{\abs{A} u}{g\s2(w,f\s2(y,u))})\\
&: (X,Z).
\end{align*}

This general cyclicity includes in particular the sliding axiom for traces from [11].
Their other axioms become simply syntactic identities in our type theory.
For instance, tightening is the statement that if we compose $f:(Y,A) \to (Z,A)$ with $u:X\to Y$ and $v:Z\to W$ and then take its trace:

*x:X u(x):Y
y:Y, a:A (f1(y,a),f2(y,a)): (Z,A)
z:Z v(z):W
x:X, a:A (v(f1(u(x),a)), f2(u(x),a)) : (W,A)
x:A (v(f1(u(x),a)) |A af2(u(x),a)) : W

we get the same result as if we first take the trace of $f$ and then compose with $u$ and $v$:

*x:X u(x):Y

*y:Y, a:A (f1(y,a),f2(y,a)): (Z,A)y:Y (f1(y,a) |A af2(y,a)) : Z

z:Z v(z):W
x:A (v(f1(u(x),a)) |A af2(u(x),a)) : W.

Since the terms concluding both derivations are the same, they represent the same morphism.
Of course, these are not actually derivations in our type theory, since they use the admissible rule of substitution.
The uniqueness of typing derivations means that if the substitutions are eliminated according to <ref> we obtain the same result in both cases, which in this case is:

x:A (u(x),a,Aa) : (Y,A,A^*)
x:A (f1(u(x),a), A a, f2(u(x),a)) : (Z,A^*,A)
x:A (v(f1(u(x),a)) |A af2(u(x),a)) : W.

Given any signature , we can augment it by adding a specified dual $A^*$ for each object $A\in\cG$ along with duality data as above.
This yields a new signature $\cG^*$ such that $\F{}\cG^*$ is freely generated by together with a specified dual for each of its object.
Thus $\F{}\cG^*$ is the free compact closed prop (i.e. prop in which every object has a dual) generated by .
Any signature of relations for carries over to $\cG^*$ as well, so we can construct presented compact closed props as well, and thereby presented compact closed monoidal categories.

In general, a prop presentation may not have any decision procedure for equality or normal forms for morphisms.
However, the view of the zigzag equalities as “$\beta$ and $\eta$ reductions” suggests that this should be the case for some classes of presented compact closed props (whenever the equalities other than the zigzag identities can be controlled).
If true, this should include in particular the explicit description of the free compact closed monoidal category on an ordinary category from [13].

Note also that by the “Int-construction” [11], any traced symmetric monoidal category embeds fully-faithfully and trace-preservingly in a compact closed one.
Thus, we can also use presented compact closed props to reason about traced symmetric monoidal categories.

§.§ Well-idempotent dualizable objects are self-dual

Tim Campion asked in [5] whether an idempotent dualizable object in a symmetric monoidal category must be self-dual.
A proof using string diagrams that this holds assuming “well-idempotence” was given by the user “MTyson”; here we recast this proof in our type theory.

We assume given one type $X$ with a dual $X^*$, expressed as before, and a morphism $i : () \to X$ such that $1_X \otimes i : X\to X\otimes X$ is an isomorphism (such an $i$ is what makes $X$ well-idempotent).
In our type theory, the latter can be expressed by a term $\types i:X$ and a morphism $x:X,y:X \types f(x,y):X$ (the inverse to $1_X \otimes i$) such that $f(x,i)= x$ and $(x,y) = (f(x,y),i)$.
More precisely, the latter two equalities are

\begin{align*}
x:X &\types f(x,i) = x : X \\
x:X, y:X &\types (x,y) = (f(x,y),i) : (X,X)
\end{align*}

but we tend to omit the contexts and types in equality axioms and calculations when they are obvious.

Note that the equation $f(x,i)=x$ means that $i$ is a “right unit” for the “binary operation” $f$.
We now observe that it is also a left unit:

\begin{align*}
&= (f(u,y) \mid \eval{\abs{X} u}{i})\\
&= (u \mid \eval{\abs{X} u}{y})\\
&= y.
\end{align*}

Here the first line is an $\beta$-expansion and the third is a $\beta$-reduction.
The second line uses the equality $(x,y) = (f(x,y),i)$ in the following way: first we introduce an extra variable to get

\[ x:X, w:X^*, y:X \types (x,w,y) = (f(x,y),w,i) : (X,X^*,X) \]

then we precompose with

\[ y:X \types (u,\abs{X}u,y) : (X,X^*,X) \]

to get

\[ y:X \types (u, \abs{X}u,y) = (f(u,y),\abs{X}u,i) : (X,X^*,X) \]

and then we post-compose with

\[ x:X, w:X^*, y:X \types (x \mid \eval{w}{y}) : X \]

to get

\[ y:X \types (u \mid \eval{\abs{X} u}{y}) = (f(u,y) \mid \eval{\abs{X} u}{i}) : X. \]

Note that although the type-theoretic justification is a bit complicated, at the level of terms the operation is intuitive: we simply simultaneously substitute $u$ for $f(u,y)$ and $y$ for $i$, wherever the latter appear as subterms.
From now on we will perform such substitutions at term-level without further comment.

Now we define $x:X \types \phi(x) :X^*$ and $w:X^* \types \psi(w):X$ by

\begin{align*}
\phi(x) &\defeq (\abs{X} v \mid \eval{\abs{X} u}{f(v,f(x,u))})\\
\psi(w) &\defeq (i \mid \eval w i).
\end{align*}

Finally, we can show that $\phi$ and $\psi$ are inverse isomorphisms (so that $X$ is isomorphic to its dual) with the following computations:

= (i |X vi, X uf(v,f(x,u)))

= (i |X uf(i,f(x,u)))      (β-reduction for v)

= (i |X uf(x,u))      (i is a left unit for f)

= (u |X ux)      ((x,u)=(f(x,u),i))

= x      (β-reduction for u)

= (X v |X uf(v,f(i,u)), w i)

= (X v |X uf(v,u), w i)      (i is a left unit for f)

= (X v |X uv, w u)      ((v,u) = (f(v,u),i))

= (X v |w v)      (β-reduction for u)

= w      (η-reduction for v).

We do not reproduce MTyson's string diagram proof here, but the reader is encouraged to compare it to our type-theoretic version.
Note that this situation is partly “topological” in the sense of <ref> (the zigzag axioms for duality, and arguably the unit properties $f(x,i)=x$ and $f(i,x)=x$) and partly non-topological (the axiom $(x,y) = (f(x,y),i)$).

§.§ Comonoids and Sweedler notation

As in ordinary cartesian (or even linear) type theory, it is easy to use our type theory to define monoid objects in a symmetric monoidal category.
The signature has one object $M$ and two morphisms $m:(M,M) \to M$ and $e:() \to M$; we usually write $m(x,y)$ infix as $x\cdot y$ or just $x y$.
The axioms are the expected

(xy)z = x(yz) xe=x ex =x.

However, with our type theory we can also define comonoid objects, which have instead two morphisms $\comult : M\to (M,M)$ and $\ep : M \to ()$, and axioms

As suggested in the introduction, this becomes much more manageable if we adopt the convention of traditional Sweedler notation for comonoids and comodules:

\[ (x\s1,x\s2) \defeq (\comult\s1(x),\comult\s2(x)) . \]

Since there is no other meaning of $Z\s i$ when $Z$ is itself already a term, it is unambiguous to regard it as meaning $\comult\s i(Z)$ as long as no type has more than one relevant comultiplication.
(We could formalize this with a more complicated type-checking algorithm, but we will be content to regard it as an informal abuse of notation.)
We may regard this as a sort of “dual” to the shorthand notation “$x y$” for multiplication in a monoid, which omits the name or symbol for the product $(M,M)\to M$.
With this notation, the axioms of a comonoid become

(xß11,xß12,x2) = (x1,xß21,xß22)

(x1 |(x2)) = x
(x2 |(x1)) = x.

Traditional Sweedler notation also goes one step further: in view of the coassociativity axiom, it is unambiguous to write $(x\s1,x\s2,x\s3)$ for either $(x\ss11,x\ss12,x\s2)$  or $(x\s1,x\ss21,x\ss22)$.
In general, if subscripts are applied to a variable or a term that is already subscripted,
with the maximum such subscript being $n$, then the subscript ${}\s k$ means $\overbrace{{}\s2{}\s2\dots{}\s2}^{k-1}{}\s1$ if $k<n$ and $\overbrace{{}\s2{}\s2\dots{}\s2}^{n-1}$ if $k=n$.

Intuitively, in cartesian type theory (i.e. in a cartesian monoidal category), everything can be duplicated and discarded with impunity; whereas a comonoid in a non-cartesian monoidal category is equipped with specified ways in which to duplicate and discard elements.
(Indeed, a cartesian monoidal category is precisely a symmetric monoidal category in which every object is equipped with a commutative comonoid structure in a natural way.)
We thus view $x\s1$ and $x\s2$ as “duplicated copies” of $x$, the subscripts tracking the order of duplication.
Similarly, we can regard $\ep(x)$ as “discarding” the element $x$, which inspires us to introduce a sort of “nullary Sweedler notation”

\[ \cancel{x} \defeq \ep(x). \]

Thus, for instance, the counit axioms of a comonoid become $(x\s1\mid \cancel{x\s2})=x$ and $(x\s2\mid \cancel{x\s1})=x$.
Note that by coassociativity, we also have equalities such as $(x\s1, x\s2 \mid\cancel{x\s3}) = (x\s1,x\s2)$ and $(x\s1, x\s3 \mid\cancel{x\s2}) = (x\s1,x\s2)$ and so on.

Such shorthands need not be restricted to comonoids either.
For instance, traditional Sweedler notation is also used for comodules, which have a coaction $D \to (C,D)$ by a coalgebra $C$.
As an example with even greater generality, suppose $M$ is dualizable and has a coaction $\comult:M\to (A,M)$, satisfying no axioms at all, and that $f:M\to M$ is an endomorphism that respects $\comult$ in that $(f(x\s1),f(x\s2)) = (f(x)\s1,f(x)\s2)$.
Then we can use this notation to verify the fixed-point property of traces from <cit.>:

\begin{align*}
(f(f(u)\s1) \mid \eval{\abs{M} u}{f(u)\s2})
&= (f(v\s1) \mid \eval{\abs{M} u}{v\s2}, \eval{\abs{M} v}{f(u)})\\
&= (f(v\s1) \mid \eval{\abs{M} v}{f(v\s2)})\\
&= (f(v)\s1 \mid \eval{\abs{M} v}{f(v)\s2}) : A.
% \\
% &= (f(u)\s1 \mid \eval{\abs{M} u}{f(u)\s2})
\end{align*}

§.§ Frobenius monoids

A Frobenius monoid is an object that is both a monoid and a comonoid and satisfies the additional axiom

\begin{equation}
x:M, y:M \types (x\s1, x\s2 y) = (x y\s1, y\s2).\label{eq:frob}
\end{equation}

Usually this is stated as two axioms saying that both sides of the above equation equal $((xy)\s1, (xy)\s2)$.
But this follows from the above axiom by the following argument, which I learned from [18]:

(x1, x2 y)
= (x1, x2 y1 |y2)           (by counitality)

= (x1, xß21 |xß22 y)           (by (<ref>))

= (xß11, xß12 |x2 y)           (by coassociativity)

= ((x y1)1, (x y1)2 |y2)           (by (<ref>))

= ((x y)1, (x y)2)           (by counitality).

The Frobenius axiom(s) are “topological”, so their string diagrams get a good deal of leverage from topological intuition.
Thus, Frobenius monoids are not a very good example for the relative usefulness of type theory.
However, for purposes of comparison, we include a proof of one of the basic facts about Frobenius monoids; namely that they are self-dual, with unit and counit:

\begin{align*}
(\eval w x) &\defeq (\,\mid \cancel{w x})\\
(\abs{M} u, u) &\defeq (e\s1, e\s2).
\end{align*}

The axioms of a dual pair follow quite easily:

(u |Mux)
(e1 |e2 x)
= (e x1 |x2)
= ex
= x

(Mu |w u)
(e2 |w e1)
= (w2 e |w1)
= w e
= w.

A hypergraph category [12] is a symmetric monoidal category in which every object is equipped with a Frobenius monoid structure that is commutative ($xy = yx$), cocommutative ($(x\s1,x\s2)=(x\s2,x\s1)$), and special a.k.a. separable ($x\s1\,x\s2 = x$), and such that the Frobenius monoid structure on any tensor product $X\otimes Y$ is induced from those on $X$ and $Y$ in the standard way.
The definition of hypergraph prop is a bit simpler: it is just a prop in which every object is equipped with a commutative, cocommutative, special Frobenius monoid structure.
Since tensor products in a prop are only formal, the final condition is essentially automatic.
More specifically, the final condition on a hypergraph category is not needed to show that it has an underlying hypergraph prop $U\cC$, but it is precisely what is needed to show that is equivalent, as a hypergraph category, to the free symmetric monoidal category generated by $U\cC$.
(One might even argue that for this reason, hypergraph props are a more natural structure than hypergraph categories.)

Now given any signature , we can augment it by adding a commutative, cocommutative, special Frobenius monoid structure on every object.
This yields a new signature $\cG^\hy$ such that $\F{}\cG^\hy$ is the free hypergraph prop generated by .
Any signature of relations for carries over to $\cG^\hy$ as well, so we can construct presented hypergraph props as well.

§.§ Hopf monoids and antipodes

A monoid object in a cartesian monoidal category is also (like every object) a comonoid, but the monoid and comonoid structures do not satisfy the Frobenius axiom.
Instead they satisfy the bimonoid axioms:

\begin{align*}
x:M,y:M &\types (x\s1 y\s1,x\s2 y\s2) = ((x y)\s1,(x y)\s2) :(M,M)\\
&\types (e\s1,e\s2)=(e,e):(M,M)\\
x:M,y:M &\types (\mid\cancel{x y}) = (\mid\cancel{x},\cancel{y}) : ()\\
&\types (\mid\cancel{e})=():().
\end{align*}

Thus, a bimonoid object in an arbitrary monoidal category can be regarded as a “non-cartesian” version of a monoid object in a cartesian monoidal category.
Indeed, if a bimonoid is cocommutative $(x\s1,x\s2) = (x\s2,x\s1)$ then it is a monoid object in the cartestian monoidal category of cocommutative comonoids, and dually if it is commutative ($xy=yx$) then it is a monoid object in the opposite of the cocartesian monoidal category of commutative monoids.
But in the non-commutative, non-cocommutative case we obtain something truly new.

The analogue for a bimonoid of the inversion operation, making a monoid into a group, is called an antipode: an operation $x:M \types \inv{x}:M$ such that

\begin{align*}
x:M &\types x\s1\, \inv{x\s2} = (e\mid\cancel{x}) :M\\
x:M &\types \inv{x\s1}\, x\s2 = (e\mid\cancel{x}) :M.
\end{align*}

A bimonoid equipped with an antipode (a non-cartesian analogue of a group object) is called a Hopf monoid.

Note that the comonoid structure is necessary in order to even formulate the antipode axioms: we need to duplicate $x$ in order to invert one copy of it, and on the other side of the equation we need to discard $x$ in order to write simply “$e$”.
In a cartesian monoidal category, Hopf monoids are precisely group objects in the usual sense.
However, note also that bimonoids and Hopf monoids in a symmetric monoidal category are self-dual: such a structure on $M\in\cC$ is equivalent to such a structure on $M\in\cC\op$.

As mentioned in the introduction, cartesian type theory can internalize the basic fact of group theory that inverses in any monoid are unique: if $\inv{x}$ and $\invt{x}$ are both inverses of $x$ the

\[ \inv{x} = \inv{x}e = \inv{x}(x\invt{x}) = (\inv{x}x)\invt{x} = e\invt{x} = \invt{x}. \]

Therefore, a monoid object in any cartesian monoidal category admits at most one inverse, and hence both cocommutative Hopf monoids and commutative ones have unique antipodes.
Cartesian type theory has nothing to say about Hopf monoids that are neither commutative nor cocommutative, but in our type theory we can reproduce essentially the same argument: if $x:M\types \inv{x}:M$ and $x:M \types \invt{x}:M$ are both antipodes, we compute

\begin{align*}
\inv{x}
= \inv{x}\, e
= (\inv{x\s1}\, e\mid\cancel{x\s2})
= \inv{x\s1}\, x\s{21} \, \invt{x\s{22}}
= (e \, \invt{x\s{2}}\mid\cancel{x\s1})
= e\, \invt{x}
= \invt{x}.
\end{align*}

Thus, 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”.
I encourage the reader to write out a proof of this fact using traditional arrow notation or string diagrams for comparison.

As another example, if $H$ and $K$ are bimonoids, a bimonoid homomorphism is a morphism $x:H \types f(x) :K$ such that

f(x y) = f(x)  f(y)(f(x)1,f(x)2) = (f(x1), f(x2))

f(e) = e (|f(x)) = (|x).

Now we can show that when $H$ and $K$ are Hopf monoids, any such bimonoid homomorphism preserves antipodes.

\begin{align*}
&= (f(\inv{x\s1}) \mid \cancel{x\s2})\\
&= (f(\inv{x\s1}) \mid \cancel{f(x\s2)})\\
&= (f(\inv{x\s1})\, e \mid \cancel{f(x\s2)})\\
&= f(\inv{x\s1})\, f(x\s2)\s1 \, \inv{f(x\s2)\s2}\\
&= f(\inv{x\s1})\, f(x\ss21) \, \inv{f(x\ss22)}\\
&= f(\inv{x\ss11})\, f(x\ss12) \, \inv{f(x\s2)}\\
&= f(\inv{x\ss11}\, x\ss12) \, \inv{f(x\s2)}\\
&= (f(e) \, \inv{f(x\s2)} \mid \cancel{x\s1})\\
&= (e \, \inv{f(x\s2)} \mid \cancel{x\s1})\\
&= (\inv{f(x\s2)} \mid \cancel{x\s1})\\
&= \inv{f(x)}.
\end{align*}

There is a more general approach to results of this sort, which we will return to in the next section.

§.§ Weak bimonoids

A weak bimonoid [18][In [18] these definitions are given in the additional generality of a braided monoidal category, but our type theory only applies to symmetric monoidal categories.
This is sufficient to include a number of examples, however, such as the category algebra of a category with finitely many objects.] is a monoid and comonoid that satisfies, instead of the bimonoid axioms, the following weakened ones:

\begin{align*}
((xy)\s1, (xy)\s2) &= (x\s1 y\s1, x\s2 y\s2)\\
(\,\mid\cancel{xyz}) &= (\,\mid \cancel{x y\s1}, \cancel{y\s2 z})\\
&= (\,\mid \cancel{x y\s2}, \cancel{y\s1 z})\\
(e\s1, e\s2, e\s3) &= (e\s1, e\s2 e'\s1, e'\s2)\\
&= (e\s1, e'\s1 e\s2 , e'\s2).
\end{align*}

For a weak bimonoid we define

\begin{align*}
s(x) &\defeq (e\s1 \mid \cancel{e\s2 x})\\
t(x) &\defeq (e\s1 \mid \cancel{x e\s2})\\
r(x) &\defeq (e\s2 \mid \cancel{e\s1 x}).
\end{align*}

Many equations relating the weak bimonoid structure and the operations $s,t,r$ are proven in [18] using string diagrams.
All of them can also be proven in our type theory.
For instance, here is a version of <cit.>:

\begin{align*}
(s(x)\s1, s(x)\s2)
&= (e\ss11, e\ss12 \mid \cancel{e\s2 x})\\
&= (e\s1, e\s2 \mid \cancel{e\s3 x})\\
&= (e\s1, e\s2 e'\s1 \mid \cancel{e'\s2 x})\\
&= (e\s1, e\s2 s(x)).
% \intertext{and dually}
% (s(x)\s1, s(x)\s2) &= (e\s1, s(x) e\s2)\\
\end{align*}

Here is a version of <cit.>:

((x  s(y))1,(x  s(y))2)
= (x1 s(y)1, x2 s(y)2)

= (x1 e1, x2 e2 s(y))      (using (1))

= ((xe)1, (xe)2 s(y))

= (x1, x2 s(y)).

And here is a version of <cit.>.

\begin{align*}
t(x)\, r(y)
&= (e\s1 e'\s2 \mid \cancel{x e\s2}, \cancel{e'\s1 y})\\
&= (e\s2 \mid \cancel{xe\s3}, \cancel{e\s1 y})\\
&= (e\s2 e'\s1 \mid \cancel{x e'\s2}, \cancel{e\s1 y})\\
&= r(y) \, t(x).
\end{align*}

As an example of a somewhat longer proof, here is a version of <cit.>.
Unlike the previous examples, this is not a verbatim translation of their proof; theirs builds on previous lemmas, whereas the below proof is direct.

(t(x1), x2 y)
= (e1, x2 y |x1 e2)

= (e1, (xe')2 y |(xe')1 e2)

= (e1, x2 e'2 y |x1 e'1 e2)

= (e1, x2 e3 y |x1 e2)

= (e1, x2 eß22 y |x1 eß21)

= (e1, (x e2)2 y |(x e2)1)

= (e1, xe2 y)

= (e1, x (e2 y)2 |(e2 y)1)

= (e1, x eß22 y2 |eß21 y1)

= (e1, x e3 y2 |e2 y1)

= (e1, x e'2 y2 |e2e'1 y1)

= (e1, x (e'y)2 |e2 (e'y)1)

= (e1, x y2 |e2 y1)

= (s(y1), x y2).

If $H$ and $K$ are weak bimonoids, a weak bimonoid homomorphism $f:H\to K$ must commute with both monoid and comonoid structures as in <ref>.
It follows that it also commutes with $s,t,r$; this is shown in <cit.>, and rendered below for $s$ in type theory:

\begin{align*}
&= (f(e\s1)\mid \cancel{e\s2 x})\\
&= (f(e\s1)\mid \cancel{f(e\s2 x)})\\
&= (f(e\s1)\mid \cancel{f(e\s2)\, f(x)})\\
&= (f(e)\s1\mid \cancel{f(e)\s2\, f(x)})\\
&= (e\s1\mid \cancel{e\s2\, f(x)})\\
&= s(f(x)).
\end{align*}

A weak bimonoid is a weak Hopf monoid if it has an antipode: a morphism $x:H \types \inv x : H$ satisfying

\begin{align*}
\inv{x\s1}\, x\s2 &= t(x)\\
x\s1 \, \inv{x\s2} &= r(x)\\
\inv{x\s1}\, x\s2\, \inv{x\s3} &= \inv{x}.
\end{align*}

This implies immediately that

x = x1  x2  x3 = x1   r(x2)x = x1  x2  x3 = t(x1)   x2.

As for ordinary bimonoids in <ref>, antipodes for weak bimonoids are unique: if $x:H \types \inv x : H$ and $x:H \types \invt x : H$ are both antipodes, we have:

\begin{align*}
\inv{x}
&= \inv{x\s1} \; r(x\s2)\\
&= \inv{x\s1} \, x\ss21 \, \invt{x\ss22}\\
&= \inv{x\ss11} \, x\ss12 \, \invt{x\s2}\\
&= t(x\s1) \, \invt{x\s2}\\
&= \invt{x}.
\end{align*}

Similarly, we can translate the argument of <cit.> that homomorphisms $f:H\to K$ of weak bimonoids preserve antipodes:

\begin{align*}
&= f(\inv{x\s1} \; r(x\s2)) \\
&= f(\inv{x\s1})\, f(r(x\s2)) \\
&= f(\inv{x\s1})\, r(f(x\s2)) \\
&= f(\inv{x\s1})\, f(x\s2)\s1 \, \inv{f(x\s2)\s2} \\
&= f(\inv{x\s1})\, f(x\ss22) \, \inv{f(x\ss22)} \\
&= f(\inv{x\ss11})\, f(x\ss12) \, \inv{f(x\s2)} \\
&= f(\inv{x\ss11}\; x\ss12) \, \inv{f(x\s2)} \\
&= f(t(x\s1)) \, \inv{f(x\s2)} \\
&= t(f(x\s1)) \, \inv{f(x\s2)} \\
&= t(f(x)\s1) \, \inv{f(x)\s2} \\
&= \inv{f(x)}.
\end{align*}

We end by sketching another approach to these sorts of uniqueness results that is inspired by the “types are like sets” perspective of our type theory.
For monoids in the category of sets, the uniqueness of inverses is a pointwise property: for any element $x$, if $y$ and $z$ are two elements that are both inverses of $x$, then $y=z$.
However, the uniqueness of antipodes as we have proven it above, for both bimonoids and weak bimonoids, is instead a statement about inversion operators that apply to all elements at once.

The pointwise statement is stronger, and this makes for simpler proofs.
For instance, we can simply show that a monoid homomorphism $f:H\to K$ preserves inverses of elements in the sense that if $y$ is an inverse of $x$ then $f(y)$ is an inverse of $f(x)$, and conclude directly from pointwise uniqueness of inverses in $K$ that $f$ of “the” inverse of $x$ coincides with “the” inverse of $f(x)$.

We can also formulate a “pointwise” sort of uniqueness of inverses in the general case.
Suppose $H$ is a weak Hopf monoid, with given antipode $x:H \types \inv{x}:H$.
Suppose also we have a comonoid $X$ and a comonoid morphism $x:X \types g(x) : H$, and also a morphism $x:X \types i(x) : H$ such that

\begin{equation}
\begin{array}{rcl}
i(x\s1)\, g(x\s2) &=& t(g(x))\\
g(x\s1) \, i(x\s2) &=& r(g(x))\\
i(x\s1) \, g(x\s2) \, i(x\s3) &=& i(x).
\end{array}\label{eq:rel-antipode}
\end{equation}

We think of $g$ as an $X$-indexed family of elements of $H$, and $i$ as a similarly indexed family of “inverses”.
Then we can calculate

t(g(x1))  i(x2)
= i(x1)  g(x2)  i(x3)
= i(x)
i(x1)  r(g(x2))
= i(x1)   g(x2)   i(x3)
= i(x)

and hence

\begin{align*}
i(x) &= i(x\s1) \, r(g(x\s2))\\
&= i(x\s1) \, g(x\s2) \, \inv{g(x\s3)}\\
% &= i(x\s1) \, g(x\ss21) \, \inv{g(x\ss22)}\\
% &= i(x\ss11) \, g(x\ss12) \, \inv{g(x\s2)}\\
&= t(g(x\s1)) \, \inv{g(x\s2)}\\
&= t(g(x)\s1) \, \inv{g(x)\s2}\\
&= \inv{g(x)}.
\end{align*}

Note that in fact it suffices for $X$ to be a co-semigroup and $g$ to be a co-semigroup morphism.
Moreover, instead of a single co-semigroup, $X$ could be a context of co-semigroups.

Applying this with $X\defeq H$ and $g(x) \defeq x$, we obtain uniqueness of the antipode itself.
But we can also derive preservation of the antipode by a weak bimonoid homomorphism $f:H\to K$, by taking $X\defeq H$ and $g\defeq f$ with $i(x)\defeq f(\inv{x})$.
We simply check that this satisfies the three properties (<ref>):

\begin{align*}
f(\inv{x\s1}) \, f(x\s2)
&= f(\inv{x\s1}\, x\s2)\\
&= f(t(x))\\
&= t(f(x)).\\
f(x\s1)\, f(\inv{x\s2})
&= f(x\s1 \, \inv{x\s2})\\
&= f(r(x))\\
&= r(f(x)).\\
f(\inv{x\s1}) \, f(x\s2) \, f(\inv{x\s3})
&= f(\inv{x\s1} \, x\s2 \, \inv{x\s3})\\
&= f(\inv{x}).
\end{align*}

Then the above argument shows immediately that $f(\inv{x}) = \inv{f(x)}$, as desired.

As a final example, we show that for a weak Hopf monoid $H$, the antipode is a weak monoid anti-homomorphism.
(Since Hopf monoids are self-dual, this implies that the antipode is also a comonoid anti-homomorphism, which was proven by a long string diagram calculation in <cit.>).
Consider how we prove the analogous statement in the category of sets, that inversion in a group is a monoid anti-homomorphism.
Arguably the most natural way is to simply check that $y^{-1} x^{-1}$ is an inverse of $x y$:

\begin{gather*}
(y^{-1} x^{-1})(x y) = y^{-1} (x^{-1} x) y = y^{-1} e y = y^{-1} y = e\\
(x y)(y^{-1} x^{-1}) = x (y y^{-1}) x^{-1} = x e x^{-1} = x x^{-1} = e
\end{gather*}

and conclude by uniqueness of inverses that $y^{-1} x^{-1} = (x y)^{-1}$.

Using our notion of pointwise uniqueness, we can reproduce this inside our type theory to apply to weak Hopf monoids.
We take $X \defeq (H,H)$, with its induced comonoid structure $x:H, y:H \types (x\s1, y\s1, x\s2, y\s2) : (H,H,H,H)$.
We define $g(x,y) \defeq xy$, which is a co-semigroup morphism (though not a comonoid morphism) by the first axiom of a weak bimonoid, and $i(x,y) \defeq \inv{y}\, \inv{x}$, and check the three properties (<ref>):

i((x,y)1)   g((x,y)2)
= y1  x1   x2   y2

= y1  t(x)   y2

= (t(x)  y)1  (t(x)  y)2      (4)

= t(t(x)  y)

= t(xy)      (3)

= t(g(x,y)).

Here the line labeled (4) uses the so-numbered equation $(y\s1,t(x)\, y\s2) = ((t(x)\,y)\s1,(t(x)\,y)\s2)$ from [18], and similarly the line (3) is an instance of their equation (3).  The next calculation is dual.

g((x,y)1) i((x,y)2)
= x1   y1   y1  x2

= x1  r(y)  x2

= (x r(y))1  (x r(y))2

= r(x r(y))

= r(xy)

= r(g(x,y)).

The final calculation uses the commutativity of $t$ with $r$, equation (13) from [18] which we also proved above.

i((x,y)1)   g((x,y)2)   i((x,y)3)
= y1  x1   x2   y2   y3  x3

= y1   t(x1)   r(y2)   x2

= y1   r(y2)  t(x1)   x2     (13)

= y   x

= i(x,y).

We leave further applications to the interested reader.

[1]
Michael Barr.
$\ast$-autonomous categories, volume 752 of Lecture Notes
in Mathematics.
Springer, 1979.

[2]
Michael Barr.
*-autonomous categories and linear logic.
Mathematical Structures in Computer Science, 1(2):159–178,

[3]
John C. Baez, Brandon Coya, and Franciscus Rebro.
Props in network theory.
arXiv:1707.08321, 2017.

[4]
R. Blute, R. Cockett, R. Seely, and T. Trimble.
Natural deduction and coherence for weakly distributive categories.
JPAA, 113:229–296, 1996.

[5]
Tim Campion.
If a $\otimes$-idempotent object has a dual, must it be self-dual?
MathOverflow, 2017.
<https://mathoverflow.net/q/277991> (version: 2017-08-09).

[6]
Luís Caires, Frank Pfenning, and Bernardo Toninho.
Linear logic propositions as session types.
Mathematical Structures in Computer Science, 26(3):367–423,

[7]
Robin Cockett and Robert Seely.
Weakly distributive categories.
Journal of Pure and Applied Algebra, 114(2):133–173, 1997.

[8]
Ross Duncan.
Types for quantum computing.
PhD thesis, Oxford University Computing Laboratory, 2006.

[9]
Peter T. Johnstone.
Sketches of an Elephant: A Topos Theory Compendium: Volumes 1
and 2.
Number 43 in Oxford Logic Guides. Oxford Science Publications, 2002.

[10]
André Joyal and Ross Street.
The geometry of tensor calculus. I.
Adv. Math., 88(1):55–112, 1991.

[11]
André Joyal, Ross Street, and Dominic Verity.
Traced monoidal categories.
Math. Proc. Cambridge Philos. Soc., 119(3):447–468, 1996.

[12]
Aleks Kissinger.
Finite matrices are complete for (dagger-)hypergraph categories.
arXiv:1406.5942, 2014.

[13]
G. M. Kelly and M. L. Laplaza.
Coherence for compact closed categories.
J. Pure Appl. Algebra, 19:193–213, 1980.

[14]
Saunders MacLane.
Categorical algebra.
Bull. Amer. Math. Soc., 71:40–106, 1965.

[15]
Saunders Mac Lane.
Categories For the Working Mathematician, volume 5 of Graduate Texts in Mathematics.
Springer, second edition, 1998.

[16]
C.-H. L. Ong.
A semantic view of classical proofs – type-theoretic, categorical,
and denotational characterizations (extended abstract).
In Proceedings of LICS '96, pages 230–241. IEEE Press, 1996.

[17]
Roger Penrose and Wolfgang Rindler.
Spinors and space-time. Vol. 1.
Cambridge Monographs on Mathematical Physics. Cambridge University
Press, Cambridge, 1984.
Two-spinor calculus and relativistic fields.

[18]
Craig Pastro and Ross Street.
Weak Hopf monoids in braided monoidal categories.
Algebra Number Theory, 3(2):149–207, 2009.

[19]
Kate Ponto and Michael Shulman.
Traces in symmetric monoidal categories.
Expositiones Mathematicae, 32(2):248–273, 2014.

[20]
Uday S. Reddy.
A typed foundation for directional logic programming.
In E. Lamma and P. Mello, editors, Extensions of Logic
Programming, pages 282–318, Berlin, Heidelberg, 1993. Springer Berlin

[21]
Peter Selinger.
A survey of graphical languages for monoidal categories.
In Bob Coeke, editor, New Structures for Physics, chapter 4.
Springer, 2011.

[22]
Masaru Shirahata.
A sequent calculus for compact closed categories, 1999.

[23]
M.E. Szabo.
Communications in Algebra, 3(8):663–689, 1975.