termderiv.tex

\documentclass{amsart}
\usepackage{amssymb,amsmath,latexsym,stmaryrd,mathtools}
\usepackage{cleveref}
\usepackage{mathpartir}
\usepackage{xcolor}
\let\types\vdash % turnstile
\def\cb{\mid} % context break
\def\cbb{\mid\mid} % context break
\def\op{^{\mathrm{op}}}
\def\p{^+} % variances on variables
\def\m{^-}
\newcommand{\e}[1]{^{\varepsilon_{#1}}}
\newcommand{\ep}{\varepsilon}
\newcommand{\shuf}{\mathrm{Shuf}}
\newcommand{\cG}{\ensuremath{\mathcal{G}}}
\newcommand{\cT}{\ensuremath{\mathcal{T}}}
\newcommand{\cJ}{\ensuremath{\mathcal{J}}}
\newcommand\un{^\times}
\let\mypm\pm
\let\mymp\mp
\def\pm{^\mypm}
\def\mp{^\mymp}
\def\ps{+} 
\def\ms{-}
\newcommand\uns{\times}
\def\pms{\mypm}
\def\jdeq{\equiv}
\def\cat{\;\mathsf{cat}}
\def\type{\;\mathsf{type}}
\def\ctx{\;\mathsf{ctx}}
\let\splits\rightrightarrows
\def\flip#1{#1^*} % reverse the variances of all variables
\def\dual#1{#1^\vee} % reverse variances *and* interchange \hat and \check
\def\mor#1{\hom_{#1}}
\def\id{\mathrm{id}}
\def\ec{\cdot} % empty context
\def\psplit{\overset{\mathsf{pair}}{\splits}}
\def\iso{\cong}
\def\tpair#1#2{#1\otimes #2}
\def\cpair#1#2{\langle #1,#2\rangle}
\def\tlet#1,#2:=#3in{\mathsf{let}\; \tpair{#1}{#2} \coloneqq #3 \;\mathsf{in}\;}
\def\clet#1,#2:=#3in{\mathsf{let}\; \cpair{#1}{#2} \coloneqq #3 \;\mathsf{in}\;}
\def\mix#1,#2 with #3 in{\mathsf{mix} {\scriptsize \begin{array}{c} \check{#1} \coloneqq \check{#3} \\ \hat{#2} \coloneqq \hat{#3} \end{array}  }\mathsf{in}\;}
\def\pcol{\overset{\scriptscriptstyle +}{:}}
\def\mcol{\overset{\scriptscriptstyle -}{:}}
\def\pmcol{\overset{\scriptscriptstyle \pm}{:}}
\def\mpcol{\overset{\scriptscriptstyle \mp}{:}}
\def\uncol{\overset{\scriptscriptstyle \times}{:}}
\def\ok{\;\mathsf{seq}}
\newcommand\vcol[1]{\overset{\scriptscriptstyle #1}{:}}
\newcommand\combine{,}
\newcommand\combineU{\sqcup}
\newcommand{\coend}{\begingroup\textstyle\int\endgroup}
\newcommand{\End}{\begingroup\textstyle\int\endgroup}
\newcommand{\Set}{\mathrm{Set}}
\newcommand{\unsigned}[1]{#1^0}
\newcommand{\joinvar}[1]{\left[#1\right]}
\newcommand{\red}[1]{\textcolor{red}{#1}}
\newcommand{\gray}[1]{\textcolor{gray}{#1}}
\newcommand\triv{\_}
\newcommand{\strto}{\curvearrowright}
\newcommand\samestring{\leftrightarrow}
\newcommand{\unif}[4]{#1\doteq #2\,\mathsf{ via }\,#3\cb #4}
\newcommand\complete{\pm}
\newcommand{\transa}[9]{\mathtt{transport}\; #1\coloneqq #2@#3 \;\mathtt{and}\; #4\coloneqq #5@#6
  \;\mathtt{to}\; #7 \;\mathtt{via}\; #8 \;\mathtt{in}\; #9}
\newcommand{\transb}[7]{\mathtt{transport}\; #1\coloneqq #2@(#3,#4) \;\mathtt{to}\; #5 \;\mathtt{via}\; #6 \;\mathtt{in}\; #7}
\mprset{flushleft}

\newtheorem{thm}{Theorem}
\newtheorem{lem}{Lemma}
\theoremstyle{definition}
\newtheorem{defn}{Definition}

\title{A directed type theory for formal category theory}
\author{Dan Licata \and Andreas Nuyts \and Patrick Schultz \and Michael Shulman}
\begin{document}
\maketitle

\section{Overview}

We take the point of view that each judgment in a type theory corresponds to a ``sort'' of object or morphism in a categorical structure, with individual such objects or morphisms represented by particular \emph{derivation trees} of that judgment.
More precisely, if the judgments can be stratified into ``levels'', such as types, terms, and equalities in finite-product theories or $\lambda$-calculus, or types, terms, propositions, and entailments in first-order logic, then each level describes a many-sorted free algebraic theory (``free'' meaning there are no axioms) whose sorts are the possible judgments and whose operations are the rules.
The free categorical structure generated by the type theory is then composed of the elements of the \emph{initial} algebras for these algebraic theories, which can be constructed as labeled trees; these are the derivation trees of type theory.

In general, the judgments of one level --- which is to say, the sorts of one of these algebraic theories --- will be defined in terms of the elements of the initial algebras at \emph{previous} levels.
For instance, in $\lambda$-calculus the first level is the types, where there is only one sort (types) and the basic operation is the binary one taking $A$ and $B$ to the function type $A\to B$.
Then the next level corresponds to morphisms, in which the judgments (sorts) are of the form $A\types B$ where $A$ and $B$ are types, i.e.\ elements of the free algebra generated by the function type operator (plus base types or type operations).

The role of a \emph{term} --- by which I include variables assigned to types in a context, and also the name of a type itself --- is to uniquely identify a derivation tree with a conciser syntax.
(This tends to be especially important when those derivation trees are being used as part of a judgment at the next level.)
The process of (perhaps) reconstructing a derivation tree from a term is \emph{type-checking}.

In the present theory we have four kinds of judgment; here they are expressed both with and without terms:
\[\begin{array}{c|c}
    \text{Without term} & \text{With term}\\\hline
    \cat & A \cat\\
    \Psi \types A & \Psi \types a:A\\
    \Psi \types \type & \Psi \types M \type\\
    \Delta \cb \Gamma \types M & \Delta \cb \Gamma\types m:M
  \end{array}\]
There is some abuse of notation here regarding contexts.
In the left column, the contexts $\Psi,\Delta,\Gamma$ denote simple lists of cats or types perhaps with variance; but in the right column, these same contexts must be annotated somehow with variables.
(As usual, $\Psi$ denotes a list of cats with variance and $\Gamma$ a list of types.
We will discuss what $\Delta$ denotes in \cref{sec:morphisms}.)

The question of \emph{how} exactly to annotate them with variables is tricky and we came up with lots of ways to do it, particularly in the last judgment.
But the point here is that the primary theory ought to be expressed in terms of the left column.
Of course, in order to \emph{describe} the rules for a later kind of judgment such as $\Delta\cb \Gamma\types M$, we have to make use of some term syntax for the previous levels; but mathematically, those rules are defined independently of whatever term syntax we might use, as long as that syntax is adequate to represent the relevant derivations.

In general, there might be \emph{multiple} ways of annotating the same derivation trees by terms; any such annotation is correct as long as a term uniquely specifies a derivation tree.
In fact, in our situation there is a ``direct'' way to annotate by terms, which leads to a ``string diagram'' style calculus, and also a ``fancier'' way to annotate that leads to more congenial terms.
But the underlying type theory, meaning the rules and hence the derivation trees and hence the free categorical structure they generate, is the same in both cases.


\section{Cats and their terms}
\label{sec:cats}

The type theory of cats and their terms is an ordinary ``linear type theory'' with two twists.
The first is that, of course, we carry variance through everywhere.
The second is that in order to make terms \emph{uniquely} determine a derivation --- and also to make the derivations describe exactly the morphisms in a free category --- we make the exchange rule admissible rather than primitive.
For if exchange were primitive, then the following two distinct derivations would yield the same term, and also ought to represent the same morphism:
\begin{mathpar}
  \inferrule*{ }{x:A, y:B \types f(x,y):C}\and
  \inferrule*[right=exchange]{\inferrule*[Right=exchange]{x:A, y:B \types f(x,y):C}{y:B,x:A \types f(x,y):C}}{x:A, y:B \types f(x,y):C}\and
\end{mathpar}

To make exchange admissible, we need to build a certain amount of permutations into the primitive rules.
Not arbitrary permutations, but ``just enough'' to obtain any desired ordering of the context of the conclusion without introducing the above sort of redundancy.
The redundancy comes from the fact that the contexts of the premises must already be free to occur in any order.
Thus, we don't want to re-build-in permutations of those, only permutations that alter the relative order between the contexts of different premises.
Formally, what we need is a \emph{shuffle}.

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

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

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

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

If $\Psi_i$ is a context of length $p_i$ for $i=1,\dots,n$, then we write $\shuf(\Psi_1,\dots,\Psi_n;\Psi)$ for the set of $(p_1,\dots,p_n)$-shuffles that act on the concatenated context $\Psi_1,\dots,\Psi_n$ to produce the context $\Psi$.
When using named variables, we assume that the variable names are preserved by this action (which means that the contexts $\Psi_1,\dots,\Psi_n$ and $\Psi$ uniquely determine such a shuffle if it exists).

Now we state the rules for this type theory.
As base/generating data, suppose we are given a ``signed multigraph'' $\cG$ of generators, consisting of a collection of objects (generating cats) and a collection of arrows (function symbols), where each arrow has a signed list of objects as its domain and a single object as its codomain.
We write $\cG(A_1\e1,\dots,A_n\e n; B)$ for the set of arrows from $(A_1\e1,\dots,A_n\e n)$ to $B$.

The first judgment ``$A\cat$'' has only \emph{one} sort as an algebraic theory; here $A$ is playing the role of a term.
We aren't currently assuming any operations on cats, so there is only one trivial rule:
\[ \inferrule{A\in\cG}{A\cat} \]
Now the second level has potential judgments (sorts in the algebraic theory) of the form $A_1\e1,\dots,A_n\e n \types B$, where the $A_i$ and $B$
are cats, and the $\ep_i$'s are either $+$ or $-$.
The primitive rules, stated without terms, are:

\begin{mathpar}
  \inferrule{A\cat}{A\p\types A}
  \and
  \inferrule{f\in \cG(A_1\e1,\dots,A_n\e n;B) \\ \Psi_i\types A_i \\
    \shuf(\Psi_1\e1,\dots\Psi_n\e n;\Phi)}{\Phi\types B}
\end{mathpar}

Here $\Psi\e{}$ is defined by $\Psi\p = \Psi$, whereas $\Psi\m$ is $\Psi$ with all variances flipped.
With terms, these rules become:

\begin{mathpar}
  \inferrule{A\cat}{x:A\p\types x:A}
  \and
  \inferrule{f\in \cG(A_1\e1,\dots,A_n\e n;B) \\ \Psi_i\types a_1:A_i \\
    \shuf(\Psi_1\e1,\dots\Psi_n\e n;\Phi)}{\Phi\types f(a_1,\dots,a_n):B}
\end{mathpar}

\begin{lem}
  Exchange is admissible: if we have a derivation of $\Psi\types A$, and a permutation $\Psi\cong \Psi'$, then we can construct a derivation of $\Psi'\types A$.
  Moreover, this operation is a group action.
\end{lem}
\begin{proof}
  Induct on the derivation of $\Psi\types A$.
  The interesting case is the second rule.
  Given its premises and a permutation $\Phi\cong\Phi'$, we decompose the composite permutation $\Psi_1\e1,\dots,\Psi_n\e n\cong \Phi\cong\Phi'$ uniquely as the block sum of $n$ permutations $\Psi_i\cong \Psi_i'$ with a shuffle ${\Psi_1'}\e1,\dots,{\Psi_n'}\e n \cong \Phi'$.
  Now by the inductive hypothesis we can derive $\Psi_i'\types A_i$ for all $i$, whence applying the same rule again with the shuffle $(\Psi_1',\dots,\Psi_n') \cong \Phi'$ we get $\Phi' \types B$.
  We likewise show that it is a group action by induction.
\end{proof}

Note that the shuffles appearing in the premises are \emph{not} notated explicitly in the terms!
Nevertheless, terms still uniquely determine derivations, because we can inspect the order that the variables appear in a term.
First we observe that the type theory is linear.

\begin{lem}\label{thm:term-linear}
  If $\Psi\types a:A$ is derivable, then every variable in $\Psi$ appears exactly once in $a$.\qed
\end{lem}

\begin{lem}\label{thm:term-deriv}
  If $a$ is a term such that $\Phi\types a:A$ is derivable, then it has a unique derivation.
\end{lem}
\begin{proof}
  By induction on derivations.
  The outer operation in a term specifies which arrow in $\cG$ must have been used in the final rule, so the question is whether this also determines all the premises uniquely.
  Inspecting a conclusion such as $\Phi \types f(a_1,\dots,a_n) : B$, we see that each variable in $\Phi$ must occur in exactly one of the terms $a_i$.
  Thus, it must be that each context $\Psi_i$ in the premises consists exactly of those variables occurring in $a_i$, and the $\ep_i$'s are determined by the arrow $f$ as well.
  Moreover, since the shuffle $\shuf(\Psi_1\e1,\dots\Psi_n\e n;\Phi)$ cannot alter the relative order of variables in $\Psi_i$, it must be that the variables in $\Psi_i$ occur in the same order as they do in $\Phi$.
  Thus the premises $\Psi_i\types a_i:A_i$ are uniquly determined.
  Finally, since the contexts $\Psi_i$ and $\Phi$ and the $\ep_i$'s are now known, the shuffle is also uniquely determined.
\end{proof}

\begin{lem}
  Cut is admissible: given derivations of $\Psi,A\e{},\Psi' \types B$ and $\Phi\types A$, we can construct a derivation of $\Psi,\Phi\e{},\Psi'\types B$.
\end{lem}
\begin{proof}
  Induction on the derivation of $\Psi,A\e{},\Psi' \types B$.
  If it is the identity, then $\ep=+$ and $B=A$, so the given $\Phi\types A$ is what we want.
  If it is obtained from a generator, then we inductively cut $\Phi\types A$ into the premise of that rule corresponding to $A$, then re-apply the generator rule.
\end{proof}

This lemma can be taken as defining the operation of substitution on terms:
\begin{align*}
  x[c/x] &= c\\
  f(a_1,\dots,a_n)[c/x] &= f(a_1,\dots,a_i[c/x],\dots,a_n)
\end{align*}
where in the second rule $a_i$ is the unique one of the $a$'s in which the variable $x$ occurs.


\section{The type judgment}
\label{sec:type-judgment}

For the third level of types, let us assume that we have given, in addition to our signed multigraph $\cG$, a set of ``base types'' each with a specified signed list of cats as domain; we write $\cT(A_1\e1,\dots,A_n\e n)$ for the set of types with this domain.
The sorts of judgment are of the form $A_1\e1,\dots, A_n\e n \types M\type$, where $A_i$ are cats and $\ep_i\in\{+,-\}$.
Here $M$ is actually a ``term'' describing the derivation tree that could be omitted from the rules, but we don't bother to write the rules without it.

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{H\in \cT(A_1\e1,\dots,A_n\e n)}{A_1\e1,\dots,A_n\e n\types \type}\;H
    \and
    \inferrule{ }{A\m, A\p \types \type}\; \mor{}
    \and
    \inferrule{
      \Psi_1 \types M_1\type \\ \Psi_2 \types M_2\type
    }{
      \Psi_1, \Psi_2 \types \type
    }\;\otimes\and
    \inferrule{
      \flip{\Psi_1} \types M_1\type \\ \Psi_2 \types M_2\type
    }{
      \Psi_1,\Psi_2 \types \type
    }\;\multimap\and
    \inferrule{\Psi \combine A\p,A\m \types M \type \\
    }{
      \Psi \types  \type
    }\;\End_{\Box} \and
    \inferrule{
      \Psi \combine A\p,A\m \types M \type \\
    }{
      \Psi \types \type
    }\;\coend^{\Box}
  \end{mathpar}
  \caption{The type judgment, without substitutions, permutations, or variables}
  \label{fig:type-nosub}
\end{figure}

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{H\in \cT(A_1\e1,\dots,A_n\e n) \\ \Psi_i\types A_i \\
      \shuf(\Psi_1\e1,\dots\Psi_n\e n;\Phi)}{\Phi\types \type}\;H
    \and
    \inferrule{\Psi_1\types A \\ \Psi_2 \types A \\ \shuf(\Psi_1\m,\Psi_2;\Phi)}{\Phi \types \type}\;\mor{}
    \and
    \inferrule{
      \Psi_1 \types M_1\type \\ \Psi_2 \types M_2\type \\ \shuf(\Psi_1,\Psi_2;\Phi)
    }{
      \Phi \types \type
    }\;\otimes\and
    \inferrule{
      \Psi_1 \types M_1\type \\ \Psi_2 \types M_2\type \\ \shuf(\Psi_1\m,\Psi_2;\Phi)
    }{
      \Phi \types \type
    }\;\multimap\\
    \inferrule{\Psi,A\p,A\m \types M \type \\
    }{
      \Psi \types \type
    }\;\End_{\Box}\and
    \inferrule{
      \Psi,A\p,A\m \types M \type \\
    }{
      \Psi \types\type
    }\;\coend^{\Box}
  \end{mathpar}
  \caption{The type judgment, with substitutions and permutations, but no variables}
  \label{fig:type-novar}
\end{figure}

We start in Figure~\ref{fig:type-nosub} with rules without built-in substitutions and permutations, and also without variables associated to cats.
In Figure~\ref{fig:type-novar} we add in the substitutions and permutations; then finally in Figure~\ref{fig:type} we add back the variables and terms.
For simplicity, we start with the ``standard'' convention whereby every cat in a context is assigned a unique variable.
Thus, the end and coend types have to bind two variables, as in the ``string diagrams'' approach.
This way, it is easy to show that the syntax of a type uniquely determines its derivation tree, just as we did for terms in the previous section (Lemmas \ref{thm:term-linear} and \ref{thm:term-deriv}).

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{H\in \cT(A_1\e1,\dots,A_n\e n) \\ \Psi_i\types a_i:A_i \\
      \shuf(\Psi_1\e1,\dots\Psi_n\e n;\Phi)}{\Phi\types H(a_1,\dots,a_n)\type}
    \and
    \inferrule{\Psi_1\types a:A \\ \Psi_2 \types b:A \\ \shuf(\Psi_1\m,\Psi_2;\Phi)}{\Phi \types \mor A(a,b) \type}
    \and
    \inferrule{
      \Psi_1 \types M_1\type \\ \Psi_2 \types M_2\type \\ \shuf(\Psi_1,\Psi_2;\Phi)
    }{
      \Phi \types M_1\otimes M_2\type
    }\and
    \inferrule{
      \Psi_1 \types M_1\type \\ \Psi_2 \types M_2\type \\ \shuf(\Psi_1\m,\Psi_2;\Phi)
    }{
      \Phi \types M_1 \multimap M_2 \type
    }\\
    \inferrule{\Psi,x:A\p,y:A\m \types M \type \\
    }{
      \Psi \types \End_{x\strto y:A} M \type
    }\and
    \inferrule{
      \Psi,x:A\p,y:A\m \types M \type \\
    }{
      \Psi \types \coend^{x\strto y:A} M \type
    }
  \end{mathpar}
  \caption{The type judgment, with substitutions, permutations, and variables with double-binding (co)ends}
  \label{fig:type}
\end{figure}

\begin{lem}\label{thm:type-linear}
  If $\Psi\types M\type$ is derivable, then every variable in $\Psi$ appears exactly once (free) in $M$.\qed
\end{lem}

\begin{lem}\label{thm:type-deriv}
  If $\Phi\types M\type$ is derivable, then it has a unique derivation.\qed
\end{lem}

We then prove the admissibility and functoriality of exchange and substitution into this judgment.
The proof of exchange is just like that for terms in the previous section.
The inductive clauses for substitution of terms are also fairly obvious; they are shown in Figure~\ref{fig:sub-types}.

\begin{figure}
  \centering
  \begin{alignat*}{2}
    \mor A(a,b)[c/x] &= \mor A(a[c/x],b) &&\qquad (x\in a)\\
    \mor A(a,b)[c/x] &= \mor A(a,b[c/x]) &&\qquad (x\in b)\\
    (M\otimes N)[c/x] &= (M[c/x] \otimes N) &&\qquad (x\in M)\\
    (M\otimes N)[c/x] &= (M \otimes N[c/x]) &&\qquad (x\in N)\\
    (M\multimap N)[c/x] &= (M[c/x] \multimap N) &&\qquad (x\in M)\\
    (M\multimap N)[c/x] &= (M \multimap N[c/x]) &&\qquad (x\in N)\\
    (\End_{x\strto y:A} N)[M/z] &= \End_{x\strto y:A} (N[M/z]) &&\qquad (x,y\notin M\quad z\neq x,y)\\
    (\coend^{x\strto y:A} N)[M/z] &= \coend^{x\strto y:A} (N[M/z]) &&\qquad (x,y\notin M\quad z\neq x,y)
  \end{alignat*}
  \caption{Substitution into types}
  \label{fig:sub-types}
\end{figure}


\section{Morphisms of types}
\label{sec:morphisms}

Last we consider the judgment for type morphisms.
This involves an ``unsigned'' type context $\Delta$.
How can we describe the shape of $\Delta$ \emph{without reference to variables}?
In addition to indicating the cats that the types depend on, $\Delta$ also has to indicate how all these dependencies are paired up with opposite variances.
Thus, before introducing variables it is reasonable to represent $\Delta$ as a list of \emph{signed} types, together with a ``pairing''.

More precisely, the potential judgments at this level (sorts of the algebraic theory) consist of:
\begin{enumerate}
\item A list of derivable type judgments $\Psi_1\types M_1\type$, \dots, $\Psi_n\types M_n\type$, plus a last one $\Phi\types N\type$.
\item A partition of the concatenated list $\Psi_1,\dots,\Psi_n,\Phi$ of signed cats into two-element subsets, in which each cat is matched with another occurrence of the same cat but with the opposite variance.
\end{enumerate}

The context $\Delta$ must contain the information of the list $\Psi_1,\dots,\Psi_n,\Phi$ together with this pairing.
When we introduce variables, the simplest way to write this is to assign a distinct variable to each signed type, as usual, and then write an extra list of pairings, such as
\[ x:A\p, y:B\m, z:B\p, w:A\m, x\strto w, z\strto y \]
If we adopt the convention that the first variable listed in each pair always has variance $+$, we can write this more concisely as
\[ x\strto w:A, z\strto y:B \]

If $\Psi$ is a signed context, we write $\Psi\strto\Psi'$ for the context obtained by duplicating each variable in $\Psi$ to a primed one in $\Psi'$, assigning it opposite variance, and then pairing each variable with its prime.
Thus, if $\Psi= (x:A\p,y:B\m)$, then $\Psi\strto\Psi'$ is $(x\strto x':A, y'\strto y:B)$.
In this situation, we write $M[']$ for the result of replacing all variables in $M$ by their primed versions.

With these conventions, the rules without any substitutions or cuts built in are shown in Figure~\ref{fig:morphism-nosub}.

\begin{figure}
\begin{mathpar}
% %% cut
% \inferrule{ (\Delta_1 \combine \Delta_2) \ctx \and
%             \Delta_1 \equiv \Psi_1 \combine \Psi_1' \and
%             \Delta_2 \equiv \Psi_2 \combine \Psi_2' \\\\
%             \Psi_1' \types M \type \and
%             \flip{\Psi_2'} \types \rho : \Psi_1' \and
%             \flip{\Psi_1} \types \Gamma_1 \ctx \and
%             \Psi_2 \types (\Gamma_2 \types N) \ok \\\\
%             \Delta_1 \cb \Gamma_1 \vdash M \and
%             \Delta_2 \cb \Gamma_2,M[\rho] \vdash N \and
%             \\\\
%             \unif{\Psi_1 \combineU \Psi_1'}{\Psi_2 \combineU \Psi_2'}{\rho}{(\Delta_0 \vdash \rho_0)} \\
%            }
%            {\Delta_0 \cb (\Gamma_1,\Gamma_2 \vdash N)[\rho_0]}
% \\
%% morphism types
\inferrule{ }
          {y \strto x : A  \cb \ec \types \mor{A}(x,y) }
\and
\inferrule{%% \Psi, x \mcol A, y \pcol A \types (\Gamma \vdash M) \ok \\
           \Delta, y \strto x' : A \cb \Gamma \vdash M\\ }
          {\Delta, x \strto x' : A , y\strto y':A \cb \Gamma, \mor{A}(x,y') \types M }

%% \inferrule {\Phi \combine x \pcol A \types M \type}
%%            {\Phi\pm \combine x \pmcol A \combine y \pmcol A\cb M,\mor{A}(x,y) \types M[y/x]
%%            }
%% \qquad
%% \inferrule {\Phi \combine y \mcol A \types M \type}
%%            {\Phi\pm \combine x \pmcol A \combine y \pmcol A\cb M,\mor{A}(x,y) \types M[x/y]
%%            }

%% tensor
\inferrule{
  \Delta \cb \Gamma,M_1,M_2 \types N
}{
  \Delta \cb \Gamma, M_1\otimes M_2 \types N
}
\and
\inferrule
    {\Phi_1 \types M_1 \type \and
      \Phi_2 \types M_2 \type
    }
    {\Phi_1\strto\Phi_1' \combine \Phi_2\strto\Phi_2' \cb M_1['] , M_2['] \types M_1 \otimes M_2}

%% coend
\inferrule{
  \Delta \combine x : A\p, y:A\m \cb \Gamma, M \types N
}{
  \Delta \cb \Gamma,\coend^{x\strto y:A} M \types N
}
\and
\inferrule{\Psi\combine x: A\p, y:A\m \vdash M \type}
          {
            \Psi \strto \Psi' \combine x'\strto y':A \cb M['] \types \coend^{x\strto y:A} M
          }

%% end
\inferrule{
  \Delta \combine x:A\p, y:A\m \cb \Gamma \types M
}{
  \Delta \cb \Gamma \types \End_{x\strto y:A} M
}
\and
\inferrule{\Psi \combine x : A\p, y:A\m \types M \type}
          {\Psi \strto \Psi' \combine x\strto y: A \cb \End_{x\strto y:A} M['] \types M}

%% hom
  \inferrule{
    \Delta \cb \Gamma, M \types N
  }{
    \Delta \cb \Gamma \types M\multimap N
  }
\and
\inferrule{
  \Phi_1 \types M_1 \type \\ 
  \Phi_2 \types M_2 \type \\ 
  }{
    \Phi_1\strto \Phi_1' ,\Phi_2\strto \Phi_2' \cb M_1['],M_1\multimap M_2['] \types M_2
  }
\end{mathpar}
\caption{Morphism judgment with no substitutions, permutations, or cuts}
\label{fig:morphism-nosub}
\end{figure}

In this syntax, the substitution rule for this judgment should be
\[
\inferrule{\Psi \types a:A \\\Delta,x\strto y:A \cb \Gamma \types M}{\Delta,\Psi\strto \Psi' \cb \Gamma[a/x,a'/y] \types M[a/x,a'/y]}
\]
where $a'$ denotes the term $a$ with all its variables primed.
Building this in in appropriate places, along with shuffles, we get the rules in Figure~\ref{fig:morphism-nocut}.

\begin{figure}
\begin{mathpar}
%% morphism types
\inferrule{\Psi \types a:A}
          {\Psi \strto \Psi'  \cb \ec \types \mor{A}(a',a) }
\and
\inferrule{\Psi\types a:A \\ \Phi\types b:A\\
           \Delta, y \strto x' : A \cb \Gamma \vdash M\\ }
          {\Delta, \Psi \strto \Psi' , \Phi\strto \Phi' \cb \Gamma[a'/x',b/y], \mor{A}(a,b') \types M[a'/x',b/y] }

%% \inferrule {\Phi \combine x \pcol A \types M \type}
%%            {\Phi\pm \combine x \pmcol A \combine y \pmcol A\cb M,\mor{A}(x,y) \types M[y/x]
%%            }
%% \qquad
%% \inferrule {\Phi \combine y \mcol A \types M \type}
%%            {\Phi\pm \combine x \pmcol A \combine y \pmcol A\cb M,\mor{A}(x,y) \types M[x/y]
%%            }

%% tensor
\inferrule{
  \Delta \cb \Gamma,M_1,M_2 \types N
}{
  \Delta \cb \Gamma, M_1\otimes M_2 \types N
}
\and
\inferrule
    {\Phi_1 \types M_1 \type \and
      \Phi_2 \types M_2 \type
    }
    {\Phi_1\strto\Phi_1' \combine \Phi_2\strto\Phi_2' \cb M_1['] , M_2['] \types M_1 \otimes M_2}

%% coend
\inferrule{
  \Delta \combine x : A\p, y:A\m \cb \Gamma, M \types N
}{
  \Delta \cb \Gamma,\coend^{x\strto y:A} M \types N
}
\and
\inferrule{\Phi \types a:A \\
           \Psi\combine x: A\p,y:A\m \vdash M \type}
          {
            \Psi \strto \Psi' \combine \Phi\strto \Phi' \cb M['][a/y',a'/x'] \types \coend^{x\strto y:A} M
          }

%% end
\inferrule{
  \Delta \combine x:A\p, y:A\m \cb \Gamma \types M
}{
  \Delta \cb \Gamma \types \End_{x\strto y:A} M
}
\and
\inferrule{\Phi \types a:A \\
           \Psi \combine x : A\p, y:A\m \types M \type}
          {\Psi \strto \Psi' \combine \Phi\strto \Phi' \cb \End_{x\strto y:A} M['] \types M[a/x,a'/y]}

%% hom
  \inferrule{
    \Delta \cb \Gamma, M \types N
  }{
    \Delta \cb \Gamma \types M\multimap N
  }
\and
\inferrule{
  \Phi_1 \types M_1 \type \\ 
  \Phi_2 \types M_2 \type \\ 
  }{
    \Phi_1\strto \Phi_1' ,\Phi_2\strto \Phi_2' \cb M_1['],M_1\multimap M_2['] \types M_2
  }
\end{mathpar}
\caption{Morphism judgment with substitutions and permutations, but no cuts}
\label{fig:morphism-nocut}
\end{figure}

Next we could try to build in enough cuts to make cut admissible in either a sequent calculus or natural deduction style, but let's skip that for now.

\section{Doubled variables}
\label{sec:doubled-var}

A nicer-looking syntax for this judgment results from writing $\coend^{x:A} M$ with the variable $x$ occurring twice in $M$.
Intuitively, this is unambiguous because one of the occurrences must be covariant and one contravariant.
We can formalize it by generalizing the entire term-assignment system (for both terms and types) to permit contexts in which each variable appears up to twice, as long as any double-occurrences are associated to the same cat with opposite variances.
Similarly, we only allow ourselves to concatenate contexts $\Psi_1\combine \Psi_2$ if the concatenated context satisfies this invariant.

Note that we are not changing the judgments, rules, or derivation trees; only the terms assigned to them and the type-checking algorithm.
With the above constraints implicit, the rules for terms and types are unchanged, except for the end and coend that now bind one variable twice rather than two different variables:
\begin{mathpar}
  \inferrule{\Psi,x:A\p,x:A\m \types M \type \\
  }{
    \Psi \types \End_{x:A} M \type
  }\and
  \inferrule{
    \Psi,x:A\p,x:A\m \types M \type \\
  }{
    \Psi \types \coend^{x:A} M \type
  }
\end{mathpar}
In general, of course, using the same variable for different types in the context would usually break the type-checking correspondence between terms and derivations.
The reason it works here is that two occurrences of a variable in a context are required to be distinguished by their variances, and we can decide by \emph{syntactic} analysis of a term or type (before type-checking it to produce a derivation) what the variance of each free occurrence of a variable therein is.

More formally, we \emph{define} inductively a notion of ``variance'' for occurrences of variables in (possibly ill-typed) terms as follows.
\begin{itemize}
\item $x$ occurs with variance $+$ in $x$.
\item If $x$ occurs in $a_i$ with variance $\ep$, and $f\in\cG(A_1\e1,\dots,A_i\e i, \dots,A_n\e n;B)$, then the induced occurrence of $x$ in $f(a_1,\dots,a_n)$ has variance $\ep\ep_i$.
\item Similarly, if $x$ occurs in $a_i$ with variance $\ep$, and $H\in\cT(A_1\e1,\dots,A_i\e i, \dots,A_n\e n)$, then the induced occurrence of $x$ in $H(a_1,\dots,a_n)$ has variance $\ep\ep_i$.
\item If $x$ occurs in $a$ with variance $\ep$, then the induced occurrence of $x$ in $\mor A(a,b)$ has variance $-\ep$.
\item If $x$ occurs in $b$ with variance $\ep$, then the induced occurrence of $x$ in $\mor A(a,b)$ has variance $\ep$.
\item If $x$ occurs in $M_1$ or $M_2$ with variance $\ep$, then the induced occurrence of $x$ in $M_1\otimes M_2$ has variance $\ep$.
\item If $x$ occurs in $M_1$ with variance $\ep$, then the induced occurrence of $x$ in $M_1\multimap M_2$ has variance $-\ep$.
\item If $x$ occurs in $M_2$ with variance $\ep$, then the induced occurrence of $x$ in $M_1\multimap M_2$ has variance $\ep$.
\item If $x$ occurs in $M$ with variance $\ep$, and $x\neq y$, then the induced occurrence of $x$ in $\End_{y:A} M$ and $\coend^{y:A} M$ has variance $\ep$.
\end{itemize}
Then we prove the following by induction on derivations.
Let $\cJ$ denote either a judgment $b:B$ or $M\type$.

\begin{lem}\label{thm:onebind-linear}
  If $\Psi \types \cJ$ is derivable, then each variable $x:A\e{}$ in $\Psi$ occurs exactly once in $\cJ$ with variance $\ep$.
  (Thus, if $x:A\p$ and $x:A\m$ both appear in $\Psi$, then $x$ occurs exactly twice in $\cJ$, once with each variance.)
\end{lem}

This enables us to show:

\begin{lem}
  If $\Psi\types \cJ$ is derivable, then it has a unique derivation.
\end{lem}
\begin{proof}
  The proof method of \cref{thm:term-deriv} (which we also used for \cref{thm:type-deriv}, without further comment) still works because of Lemma \ref{thm:onebind-linear}.
  For instance, consider a judgment $\Psi\types M\otimes N \type$.
  If this is derivable, then each variable $x:A\e{}$ in the context occurs exactly once in $M\otimes N$ with variance $\ep$, hence in exactly one of $M$ and $N$ with that variance.
  (The fact that we might also have $x$ appearing with a different variance elsewhere doesn't matter.)
  Thus, the context $\Psi$ splits uniquely as a shuffle of a context for $M$ and a context for $N$, and the induction proceeds as before.
\end{proof}

We can prove admissibility of exchange as before.
Substitution is a little more subtle to state since variables can occur more than once:

\begin{lem}
  Let $\Psi$ be a context not containing the variable $x$ at all.
  \begin{enumerate}
  \item If $\Psi,x:A\e{} \types \cJ$ and $\Phi \types a:A$, then $\Psi,\Phi\e{} \types \cJ[a/x]$ (assuming the context $\Psi,\Phi\e{}$ is valid).
  \item If $\Psi,x:A\p,x:A\m \types \cJ$ and $\Phi \types a:A$, then $\Psi,\Phi,\Phi\m \types \cJ[a/x]$ (assuming the context $\Psi,\Phi,\Phi\m$ is valid, which means that $\Phi$ has no doubled variables and none of its variable occur in $\Psi$ either).\qed
  \end{enumerate}
\end{lem}

We also need to be able to ``coalesce'' distinct variables:

\begin{lem}
  Let $\Psi$ be a context not containing the variables $x$, $y$, or $z$.
  If we can derive $\Psi,x:A\p,y:A\m \types \cJ$, then also $\Psi,z:A\p,z:A\m \types \cJ[z/(x,y)]$.\qed
\end{lem}

Here $\cJ[z/(x,y)]$ just means that we substitute $z$ for both $x$ and $y$; we write it with a special notation to emphasize that what's happening is a little different from a substitution $\cJ[z/x,z/y]$ in ordinary type theory, since $z$ still appears twice in the context.
For brevity, we write $\cJ[a/(x,y)]$ for $\cJ[z/(x,y)][a/z]$.
We also write $\cJ[z/(x,y)]$ in cases where it is unknown whether both $x$ and $y$ appear in $\cJ$, with the intent that if only one appears then we mean $\cJ[z/x]$ or $\cJ[z/y]$, and if none appears we just mean \cJ.

Now for the morphism judgment, we can take our contexts $\Delta$ to be ordinary-looking ones in which each variable occurs only once, \emph{without} variances.
Implicitly, we view each such variable as occurring twice, with both variances, and ``paired with itself''.
Thus, $x:A,y:B$ will mean something like ``$x\strto x:A, y\strto y:B$'' in our previous notation (but of course in \cref{sec:morphisms} we didn't allow multiple occurrences of the same variable).
The important thing is that with our current term-assignment system, these contexts carry exactly the same information as the $\Delta$'s with string-diagram-style pairings from \cref{sec:morphisms}.

With this convention, the rules from \cref{fig:morphism-nocut} become those in \cref{fig:morphism-dblvar}.
We write $\unsigned{\Psi}$ for the unsigned context obtained from a signed context $\Psi$ by discarding all the variances; this corresponds to the ``doubled'' context $\Psi\strto\Psi'$ from \cref{sec:morphisms}.

\begin{figure}
\begin{mathpar}
%% morphism types
\inferrule{\Psi \types a:A}
          {\unsigned{\Psi} \cb \ec \types \mor{A}(a,a) }
\and
\inferrule{\Psi\types a:A \\ \Phi\types b:A\\
           \Delta, z:A \cb \Gamma[z/(x,y)] \vdash M[z/(x,y)]}
          {\Delta, \unsigned\Psi, \unsigned\Phi \cb \Gamma[a/x,b/y], \mor{A}(a,b) \types M[a/x,b/y] }

%% \inferrule {\Phi \combine x \pcol A \types M \type}
%%            {\Phi\pm \combine x \pmcol A \combine y \pmcol A\cb M,\mor{A}(x,y) \types M[y/x]
%%            }
%% \qquad
%% \inferrule {\Phi \combine y \mcol A \types M \type}
%%            {\Phi\pm \combine x \pmcol A \combine y \pmcol A\cb M,\mor{A}(x,y) \types M[x/y]
%%            }

%% tensor
\inferrule{
  \Delta \cb \Gamma,M_1,M_2 \types N
}{
  \Delta \cb \Gamma, M_1\otimes M_2 \types N
}
\and
\inferrule
    {\Phi_1 \types M_1 \type \and
      \Phi_2 \types M_2 \type
    }
    {\unsigned{\Phi_1} \combine \unsigned{\Phi_2} \cb M_1 , M_2 \types M_1 \otimes M_2}

%% coend
\inferrule{
  \Delta \combine x : A\p, x:A\m \cb \Gamma, M \types N
}{
  \Delta \cb \Gamma,\coend^{x:A} M \types N
}
\and
\inferrule{\Phi \types a:A \\
           \Psi\combine x: A\p,x:A\m \vdash M \type}
          {
            \unsigned{\Psi} \combine \unsigned{\Phi} \cb M[a/x] \types \coend^{x:A} M
          }

%% end
\inferrule{
  \Delta \combine x:A\p, x:A\m \cb \Gamma \types M
}{
  \Delta \cb \Gamma \types \End_{x:A} M
}
\and
\inferrule{\Phi \types a:A \\
           \Psi \combine x : A\p, x:A\m \types M \type}
          {\unsigned{\Psi} \combine \unsigned{\Phi} \cb \End_{x:A} M \types M[a/x]}

%% hom
  \inferrule{
    \Delta \cb \Gamma, M \types N
  }{
    \Delta \cb \Gamma \types M\multimap N
  }
\and
\inferrule{
  \Phi_1 \types M_1 \type \\ 
  \Phi_2 \types M_2 \type \\ 
  }{
    \unsigned{\Phi_1} ,\unsigned{\Phi_2} \cb M_1,M_1\multimap M_2 \types M_2
  }
\end{mathpar}
\caption{Morphism judgment with doubled variables}
\label{fig:morphism-dblvar}
\end{figure}

\end{document}