resource2.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\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\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}


\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}

\begin{mathpar}
\begin{array}{l}
v :: = \ps \mid \ms \\
\Psi,\Delta,\Phi ::= \cdot \mid \Psi_1 \combine \Psi_2 \mid  x \vcol v A \\
\\ 
\Gamma ::= \cdot \mid \Gamma, M\\
\end{array}
\end{mathpar}

We write $\flip{v}$ for flipping a variance:
\[
\begin{array}{lll}
\flip{\ps} & := & \ms \\
\flip{\ms} & := & \ps \\
\end{array}
\]

Judgements:

\begin{itemize}

\item $A \cat$

\item $\Psi \ctx$

\item $\Psi \types a : A$

\item $\Psi \types M \type$

\item $\Psi \types \Gamma \ctx$

\item $\Psi \types (\Gamma \vdash M) \ok$

\item $\Delta \cb \Gamma \vdash M$, presupposes 
 $\Delta \types (\Gamma \vdash M) \ok$.  

\end{itemize}

\section{Category Language with Explicit Substitutions}

\subsection{Category Contexts}

Category contexts can be thought of as finite sets of triples $(x,v,A)$
with the constraint that each $x$ either occurs once, or occurs twice
with the same $A$ and opposite $v$.  We represent these sets as
quotiented trees.  

Category contexts $\Psi$ are defined inductively-recursively with a
relation $x \vcol v A \in \Psi$, which means the variable $x$ can be
used with variance $v$.

\begin{mathpar}
\inferrule{ }{\ec \ctx}

\inferrule{ }{(x \vcol v A) \ctx}

\inferrule{ \Psi_1 \ctx \and \Psi_2 \ctx \\\\
            (\forall x,v_1,v_2,A_1,A_2. \: (x \vcol {v_1} A_1) \in \Psi_1
            \text{ and } (x \vcol {v_2} A_2 \in \Psi_2)
            \text{ implies } A_1 = A_2 \text{ and } \flip{v_1} = v_2)
          }
          {\Psi_1 \combine \Psi_2 \ctx}
\end{mathpar}
The combination of two contexts is defined when any variable that is in
both occurs with the same type and opposite variance.  

Membership is defined by recursion:
\[
\begin{array}{lll}
x \vcol v A \in (x \vcol {v'} A') & \text{ iff } & v = v' \text{ and } A = A' \\
x \vcol v A \in {(\Psi_1 \combine \Psi_2)} & \text{ iff } & 
x \vcol{v} A \in \Psi_1, \text{ or } x \vcol{v} A \in \Psi_2
\end{array}
\]
We write $x \pmcol A$ for $(x \pcol A) \combine (x \mcol A)$.

We write $\Delta$ for a context where every variable is $\pms$ ($\forall
x \vcol{v} A \in \Delta, x \vcol{\flip{v}} A \in \Delta$), and $\Phi$
for a context where no variable is $\pms$ ($\forall x \vcol{v} A \in
\Phi, \neg (x \vcol{\flip{v}} A \in \Phi)$).  Note that $\Phi \combine
\flip{\Phi}$ is always well-formed and is a $\Delta$; we write
$\Phi\complete$ for this.  

To mod out by order and associativity, we make contexts into a
commutative monoid by the congruence generated by
\begin{mathpar}
\inferrule{ }
          { \Psi_1 \combine \Psi_2 \equiv \Psi_2 \combine \Psi_1}
\qquad
\inferrule{ }
          { (\Psi_1 \combine \Psi_2) \combine \Psi_3 \equiv \Psi_1 \combine (\Psi_2 \combine \Psi_3)}
\qquad
\inferrule{ }
          { \cdot \combine \Psi \equiv \Psi}
\qquad
\inferrule{ }
          { \Psi \combine \cdot \equiv \Psi}
\end{mathpar}

This should have the property that (1) one side is well-formed iff the
other is, and (2) $x \vcol v A \in \Psi_1$ iff $x \vcol v A \in \Psi_2$
when $\Psi_1 \equiv \Psi_2$.  FIXME check.  

All future judgements are defined on equivalence classes of contexts.  

We can define an involution
\begin{mathpar}
\inferrule*[right=admissible]
           {\Psi \ctx}
           { \flip{\Psi} \ctx
           }

x \vcol r A \in {\flip \Psi} \text{ iff } x \vcol {\flip{r}} A \in \Psi 
\end{mathpar}
by
\[
\begin{array}{l}
\flip{\cdot} = \cdot \\
\flip{(x \vcol v A)} = x \vcol {\flip v} A \\
\flip{(\Psi_1 \combine \Psi_2)} = {\flip{\Psi_1}} \combine {\flip{\Psi_2}} \\
\end{array}
\]
This satisfies $\flip{(\flip \Psi)} = \Psi$.  FIXME: Check all this, and
check that this is defined on equivalence classes.

Our judgement is a bit unusual, in that a variable $x$ can be ``bound''
more than once in the context.  This disturbs the usual story about
$\alpha$-conversion, which is that the occurence of $x$ in $\Gamma, x :
A , \Gamma' \vdash J$ binds $x$, which is what justifies
``horizontally'' $\alpha$-convert to $\Gamma, y : A , \Gamma'[y
  \leftrightarrow x] \vdash J[y \leftrightarrow x]$, renaming all
references to $x$.  Nonetheless, we would like all judgements here to
horizontally $\alpha$-convert, in the sense that $\Psi \vdash J$ and
$\Psi[x \leftrightarrow y] \vdash J [x \leftarrow y]$ are identified.
This could be formalized in various ways: (1) we could represent
variables by names/atoms in a nominal framework and arrange for
everything to be invariant under permutation of names.  (2) We could
think of $\Psi$ as coming with a separate context binding the names, so
the judgement really means $(x_1,x_2,\ldots,x_n);\Psi \vdash J$ where
the variables are all bound up front, and the occurrences in the context
are now \emph{bound} occurrences.  We can suppress this in the notation,
because the generality context can always be inferred from $\Psi$---so
when we write a $\Psi$, we could think of it as implicitly coming with
the ``domain'' of variables that are bound.

\subsection{Context Isomorphisms}

A renamings between $\Psi$ and $\Psi'$ represents a bijection between $x
\vcol b A \in \Psi$ and $y \vcol b A \in \Psi'$.  We present them as
trees of $x/y^b$ bindings, quotiented by associativity, commutativity,
and unit.  

\begin{mathpar}
\inferrule{ }
          {\cdot \vdash \cdot : \cdot}
\and
\inferrule{ }
          { x \vcol v A \vdash x/y^v : y \vcol v A}
\and 
\inferrule{ \Psi_1 \vdash \rho_1 : \Psi_1'  \\
            \Psi_2 \vdash \rho_2 : \Psi_2' \\
           }
          { \Psi_1 \combine \Psi_2 \vdash (\rho_1 \combine \rho_2) : \Psi_1' \combine \Psi_2'}
\and
\inferrule{ }
          {\Psi \vdash 1_\Psi : \Psi }
\and
\inferrule{\Psi \vdash \rho' : \Psi' \and
            \Psi' \vdash \rho : \Psi''}
          {\Psi \vdash \rho[\rho'] : \Psi'' }
\and
\inferrule{\Psi \vdash \rho' : \Psi'}
          {\Psi' \vdash \rho'^{-1} : \Psi}
\and 
\inferrule{\Psi \vdash \rho : \Psi'}
          {\flip{\Psi} \vdash \flip{\rho} : \flip{\Psi'} }
\end{mathpar}

We define an equational theory on renamings as the congruence generated
by the following axioms.  First, in the judgement $\Psi \vdash \rho :
\Psi'$, $\Psi$ and $\Psi'$ are considered up to $\equiv$, and we impose
associativity/commutativity/unit on renamings:
\begin{mathpar}
\inferrule{ }
          { \rho_1 \combine \rho_2 \equiv \rho_2 \combine \rho_1}
\qquad
\inferrule{ }
          { (\rho_1 \combine \rho_2) \combine \rho_3 \equiv \rho_1 \combine (\rho_2 \combine \rho_3)}
\qquad
\inferrule{ }
          { \cdot \combine \rho \equiv \rho}
\qquad
\inferrule{ }
          { \rho \combine \cdot \equiv \rho}
\end{mathpar}

We also have definitions for identity, inverse, composition, and
flipping, and the groupoid/involution laws:
\begin{mathpar}
\begin{array}{rcl}
1_\cdot & \equiv & \cdot \\
1_{x \vcol v A} & \equiv & x/x^v\\
1_{\Psi_1,\Psi_2} & \equiv & 1_{\Psi_1},1_{\Psi_2}\\
\end{array}
\quad
\begin{array}{rcl}
\cdot^{-1} & \equiv & \cdot\\
(x/y^v)^{-1} & \equiv & y/x^v\\
(\rho_1,\rho_2)^{-1} & \equiv & \rho_1^{-1},\rho_2^{-1}\\
\end{array}
\quad
\begin{array}{rcl}
\flip{\cdot} & \equiv & \cdot\\
\flip{(x/y^v)} & \equiv & x/y^{\flip v}\\
\flip{(\rho_1,\rho_2)} & \equiv & \flip{\rho_1},\flip{\rho_2}\\
\end{array}

\begin{array}{rcll}
\cdot[\rho'] & \equiv & \cdot \\
(x/y^v)[\rho'] & \equiv & z/y^v & \text{ if } \rho \equiv z/x^v \\
(\Psi_1' \vdash \rho_1, \Psi_2' \vdash \rho_2)[\rho'] & \equiv &
\rho_1[\rho_1'],\rho_2[\rho_2'] & \text{ if } \rho' \equiv (\rho_1' : \Psi_1',\rho_2' : \Psi_2') \\
\end{array}

\begin{array}{rcl}
1[\rho] & \equiv & \rho \\
\rho[1] & \equiv & \rho \\
(\rho[\rho'])[\rho''] & \equiv & \rho[\rho'[\rho'']] \\
\rho^{-1}[\rho] & \equiv & 1 \\
\rho[\rho^{-1}] & \equiv & 1 \\
\flip{{\flip{\rho}}} & \equiv & \rho \\
\end{array}
\end{mathpar}

All future judgements are implicitly defined on $\equiv$-classes of
renamings.

\paragraph{Splitting} Given $\Psi \vdash \rho : \Psi_1' \combine \Psi_2'$, 
there exist (unique up to $\equiv$) $\Psi_1$ and $\Psi_2$ and $\rho_1$
and $\rho_2$ such that $\Psi \equiv \Psi_1 \combine \Psi_2$ and $\Psi_1
\vdash \rho_1 : \Psi_1'$ and $\Psi_2 \vdash \rho_2 : \Psi_2'$ and
$\rho_1 \combine \rho_2 \equiv \rho$.  Informally, $\rho_1$ contains all
bindings $y/x^b$ from $\rho$ for $x \vcol b A \in \Psi_1$ and $\rho_2$
contains all bindings $y/x^b$ from $\rho$ for $x \vcol b A \in \Psi_2$;
we could also write this out formally as an operation on trees.

\subsection{Unification of Renamings}

We introduce a new judgement and rules for deriving valid string diagram
compositions. The new judgement has the form 
\[
\unif{(\Psi_1 \combineU \Psi_1')} {(\Psi_2 \combineU \Psi_2')} {\rho} {(\Delta_0 \vdash \rho_0)}
\]
under the presupposition that there exist $\Delta_1$ and $\Delta_2$ and
$\Delta$ such that $\Delta_1 \equiv \Psi_1 \combine \Psi_1'$ and $\Delta_2 =
\Psi_2 \combine \Psi_2'$ and $\Delta \equiv \Delta_1 \combine \Delta_2$
(i.e. $\Psi_1 \combine \Psi_1'$ exists and is a $\pms$-context, the same
for $\Psi_2 \combine \Psi_2'$, and these are independent) and
$\flip{\Psi_2'} \types \rho : \Psi_1'$ and $\Delta_0 \vdash \rho_0 :
\Psi_1 \combine \Psi_2$.  This should be read as stating that $\Delta_0$
is the result of composing $\Delta_1$ and $\Delta_2$ by gluing along
$\rho$, and that the composition introduced no loops.

%% Formally, this judgement is a
%% relation on $(\Psi,d_1,v_1,v_1',d_2,v_2,v_2',\rho,d,\rho_0)$---$\Psi$
%% occuring three times and the $=$ and $\combine$ and $\vdash$ in the
%% judgement are just notation.

The rules for this judgement are
\begin{small}
\begin{mathpar}
  \inferrule{ }
            {
              \unif{(\Delta_1 \combineU \cdot)}{(\Delta_2 \combineU \cdot)}{\cdot}{({\Delta_1 \combine \Delta_2} \vdash 1)}
            }

  \inferrule{
    \unif{(\Psi_1 \combineU \Psi_1')}{(\Psi_2 \combineU \Psi_2')}{\rho}{(\Delta_0 \vdash \rho_0)}
  }{
    \unif{((\Psi_1 \combine {x \vcol {\flip v} A}) \combineU (\Psi_1' \combine {x \vcol v A}))}
         {((\Psi_2 \combine {y \vcol {v} A}) \combineU (\Psi_2' \combine {y \vcol {\flip v} A}))}
         {(\rho \combine (y/x^v))}
         {(\Delta_0 \combine x \pmcol A \vdash \rho_0 \combine (x/x^{\flip{v}}) \combine (x/y^{v}))}
  }

  \inferrule{
    [  (\Delta_2 \combine x \pmcol A \combine y \pmcol A) \equiv \Psi_2 \combine (\Psi_2' \combine x \pcol A \combine y \mcol A) ]\\\\
    ((\Delta_2 \combine x \pmcol A) \vdash (1_{\Delta_2} \combine
    x/x\m \combine x/y\p) : (\Psi_2 \combine \Psi_2')) \equiv (\Psi_3 \vdash \rho_3 : \Psi_2) \combine (\Psi_3' \vdash \rho_3' : \Psi_2')\\\\
    \unif{\Psi_1 \combineU \Psi_1'}{\Psi_3 \combineU \Psi_3'}{\rho[\flip{\rho_3'}]}{(\Delta_0 \vdash \rho_0)}
  }{
    \unif{\Psi_1 \combineU (\Psi_1' \combine z \pmcol A)} %% {\Psi^{d_1\combine z\pm = v_1 \combine (v_1' \combine z\pm)}}
         {\Psi_2 \combineU (\Psi_2' \combine x \pcol A \combine y \mcol A)}
         {(\rho \combine x/z\m \combine y/z\p)}
         {(\Delta_0 \vdash (1_{\Psi_1} \combine \rho_3)[\rho_0])}
  }

  \inferrule{
    [  (\Delta_1 \combine x \pmcol A \combine y \pmcol A) \equiv \Psi_1 \combine (\Psi_1' \combine x \pcol A \combine y \mcol A) ]\\\\
    (1_{\Delta_1} \combine (x/x\m \combine x/y\p)) \equiv (\Psi_3 \vdash \rho_3 : \Psi_1 , \Psi_3' \vdash \rho_3' : \Psi_1' ) \\\\
        \unif{\Psi_3 \combineU \Psi_3'}{\Psi_2 \combineU \Psi_2'}{\rho_3'^{-1}[\rho]}{(\Delta_0 \vdash \rho_0)}
  }{
    \unif{\Psi_1 \combineU (\Psi_1' \combine x \pcol A \combine y \mcol A)}
         {\Psi_2 \combineU (\Psi_2' \combine z \pmcol A)}
         {(\rho \combine z/x\p \combine z/y\m)}
         {(\Delta_0 \vdash (1 \combine \rho_3)[\rho_0])}
  }
\end{mathpar}
\end{small}

The first (bracketed) premise on the third and fourth rules is really
part of the implicit arguments to the conclusion, but it doesn't fit on
the bottom line---i.e. $\Delta_1$ and $\Delta_2$ are really given, and
these rules only apply when they are of a certain form.  The second
premises cannot fail; they're just defining $\rho_3$ and $\rho_3'$ to be
the partitioning of the renaming on the left, which sends the $x/x$ and
$x/y$ to the appropriate side.  

%% FIXME update description

%% Reading the rules bottom-to-top as an algorithm for finding $d$ and
%% $\rho_0$, to get the recursion to go through, it seems necessary to
%% process the renaming $\rho$ in the conclusion by \emph{splitting} it,
%% not by case-analyzing it as $\rho,\vec{x}/x$.  This way, the premises
%% are in the same context $\Psi$ as the conclusion, but under different
%% resources.  If we case-analyze as $\rho,\vec{x}/x$, then we would need
%% to generalize the operation somehow, because the codomain of $\rho$
%% would be different of a different length than its domain.  The judgement
%% is therefore non-deterministic, because the same renaming can be split
%% in many different ways.  Conjecture: all of the results are isomorphic.

%% We write $b$ for $\ps$ or $\ms$.  We write $\Psi^{y^b} \types y/x :
%% \Psi^{x^v}$ for the renaming given by $y/x$ along with $\triv/z$ for
%% every other $z \in \Psi$ (formally, this has to be defined by induction
%% on $\Psi$).

%% Operationally, we think of $\Psi,d_1,v_1,v_1',d_2,v_2,v_2',\rho$ as
%% inputs, and $d,\rho_0$ as outputs.  FIXME: when can the rules fail?

%% In the first rule, if the given splitting puts all the resources in
%% $v_1$ and $v_2$, and $v_1'$ and $v_2'$ are $\uns$ in each component,
%% then $\rho$ can only consist of $\triv/x$ for each variable $x$.  In
%% this case, we return the identity renaming.

%% Draw $d_1 = v_1 \combine v_1'$ and $d_2 = v_2 \combine v_2'$ like in
%% Patrick's email, with vertical columns for the aspects in $v_1$, $v_1'$,
%% $v_2'$, and then $v_2$ from left to right.  We say that the $v_1'$ and
%% $v_2'$ aspects are ``internal'' and the $v_1$ and $v_2$ are external
%% (they will be in the boundary of the result, but maybe connected up).

%% Rule 2: if the given $d_1$ and $d_2$ each have a distinguished variable
%% $x$ (split with half going in $v_1$ and the other half in $v_1'$) and
%% $y$ (split with half going in $v_2$ and the other half in $v_2'$), and
%% the renaming splits to include $y/x$, then we are joining the $x$ string
%% and the $y$, so we want to identify the external $x$ and $y$ in the
%% output.  Plugging in the two sides of $x$ for $x$ and $y$ by merging
%% with the renaming $\Psi^{x\pm = x^{\flip{v}} \combine x^v} \vdash (x/x
%% \combine x/y) : \Psi^{x^{\flip v} \combine y^{b}}$ does this.

%% Rule 3: Two variables on the right are getting glued together by an
%% internal line on the left.  Why it type checks: We have
%% $\Psi^{\flip{v_2'}} \vdash \rho : \Psi^{v_1'}$ and $d_2 \combine (x\m
%% \combine y\p) = v_2 \combine v_2'$.  However, we can't make a recursive
%% call with this, because $d_2 \combine (x\m \combine y\p)$ is not
%% $d$-context, so we first need to merge $x$ and $y$.  $x$ and $y$ might
%% occur in either $v_2$ or $v_2'$, so it seems like we need to do a bunch
%% of cases, to see where to do the substitution.  However, a slick way to
%% handle this is to start with the renaming
%% \[
%% \Psi^{d_2 \combine x\pm} \vdash (1_{d_2} \combine (x/x \combine x/y)) : \Psi^{d_2 \combine (x\m \combine y\p)}
%% \]
%% and then split it along the known context splitting 
%% $d_2 \combine (x\m \combine y\p) = v_2 \combine v_2'$.
%% to get
%% \begin{mathpar}
%% d_2 \combine x\pm = v_3 \combine v_3' \and
%% \Psi^{v_3} \vdash \rho_3 : \Psi^{v_2} \and
%% \Psi^{v_3'} \vdash \rho_3' : \Psi^{v_2'}
%% \end{mathpar}
%% This will push the appropriate part of $x/x$ and $x/y$ into the
%% appropriate half.  Then   
%% \begin{mathpar}
%% \Psi^{\flip{v_3'}} \vdash \rho[\flip{\rho_3'}] : \Psi^{v_1'}
%% \end{mathpar}
%% so we can recur, getting 
%% \begin{mathpar}
%% \Psi^{d} \vdash \rho_0 : \Psi^{v_1 \combine v_3}
%% \end{mathpar}
%% Finally we compose with 
%% \begin{mathpar}
%% \Psi^{v_1 \combine v_3} \vdash 1_{v_1} \combine \rho_3 : \Psi^{v_1 \combine v_2}
%% \end{mathpar}
%% to get the result.

%% FIXME: it seems arbitrary that we pick $x$ and not $y$ here?

%% Rule 4: This is symmetric to rule 3, except here two variables on the
%% left are getting glued together by an internal line on the right.  
%% The code is basically dual, except we use $p_3'^{-1}$.  

%% FIXME: how exactly does this preclude loops?

\subsection{Substitutions}

\begin{mathpar}
\inferrule{ }
          {\cdot \vdash \cdot : \cdot}
\and
\inferrule{ \Psi^v \vdash a : A}
          { \Psi \vdash a/x^v : x \vcol v A}
\and 
\inferrule{ \Psi_1 \vdash \theta_1 : \Psi_1'  \\
            \Psi_2 \vdash \theta_2 : \Psi_2' \\
           }
          { \Psi_1 \combine \Psi_2 \vdash (\theta_1 \combine \theta_2) : \Psi_1' \combine \Psi_2'}
\\\\
\inferrule{ }
          {\Psi \vdash 1_\Psi : \Psi }
\and
\inferrule{\Psi \vdash \theta' : \Psi' \and
           \Psi' \vdash \theta : \Psi''}
          {\Psi \vdash \theta[\theta'] : \Psi'' }
\and 
\inferrule{\Psi \vdash \theta : \Psi'}
          {\flip{\Psi} \vdash \flip{\theta} : \flip{\Psi'} }
\end{mathpar}

The equations on substitutions are analogous to renamings:
\begin{mathpar}
\inferrule{ }
          { \theta_1 \combine \theta_2 \equiv \theta_2 \combine \theta_1}
\qquad
\inferrule{ }
          { (\theta_1 \combine \theta_2) \combine \theta_3 \equiv \theta_1 \combine (\theta_2 \combine \theta_3)}
\qquad
\inferrule{ }
          { \cdot \combine \theta \equiv \theta}
\qquad
\inferrule{ }
          { \theta \combine \cdot \equiv \theta}

\begin{array}{rcl}
1_\cdot & \equiv & \cdot \\
1_{x \vcol v A} & \equiv & x/x^v\\
1_{\Psi_1,\Psi_2} & \equiv & 1_{\Psi_1},1_{\Psi_2}\\
\end{array}

\begin{array}{rcll}
\cdot[\theta] & \equiv & \cdot \\
(a/y^v)[\theta] & \equiv & a[\theta^v]/y^v \\
(\Psi_1' \vdash \theta_1, \Psi_2' \vdash \theta_2)[\theta'] & \equiv &
\theta_1[\theta_1'],\theta_2[\theta_2'] & \text{ if } \theta' \equiv (\theta_1' : \Psi_1',\theta_2' : \Psi_2') \\
\end{array}

\begin{array}{rcl}
\flip{\cdot} & \equiv & \cdot\\
\flip{(a/y^v)} & \equiv & a/y^{\flip v}\\
\flip{(\theta_1,\theta_2)} & \equiv & \flip{\theta_1},\flip{\theta_2}\\
\end{array}

\begin{array}{rcl}
1[\theta] & \equiv & \theta \\
\theta[1] & \equiv & \theta \\
(\theta[\theta'])[\theta''] & \equiv & \theta[\theta'[\theta'']] \\
\flip{{\flip{\theta}}} & \equiv & \theta \\
\end{array}
\end{mathpar}

\paragraph{Splitting} Like for renamings, given $\Psi \vdash \theta : \Psi_1' \combine \Psi_2'$, 
there exist unique (up to $\equiv$) $\Psi_1$ and $\Psi_2$ and $\theta_1$
and $\theta_2$ such that $\Psi \equiv \Psi_1 \combine \Psi_2$ and
$\Psi_1 \vdash \theta_1 : \Psi_1'$ and $\Psi_2 \vdash \theta_2 :
\Psi_2'$ and $\theta_1 \combine \theta_2 \equiv \theta$.  Informally,
$\theta_1$ contains all $a/x^b$ from $\rho$ where $x \vcol b A \in
\Psi_1$ and $\theta_2$ contains all $a/x^b$ from $\rho$ where $x \vcol b
A \in \Psi_2$.

%% For example, the following rule is derivable, and is the analogue of the
%% $(\check{a}/\check{x},\hat{a}/\hat{x})$ substitution in the other
%% version.  
%% \begin{mathpar}
%% \inferrule*[right=derivable]
%%            {\Psi^{v'} \vdash \theta : \Psi'  \\
%%              \Psi^{p} \vdash a : A \\
%%              v = {v'} \combine {(\flip{p} \combine p)} \\
%%            }
%%            {\Psi^{v} \vdash (\theta,(a,a)/x) : (\Psi',x \pmcol A)}
%% \end{mathpar}
%% On the other hand, a substitution $(\theta,(a,b)/x)$ is like
%% $(a/\check{x},b/\hat{x})$.

%% \subsubsection*{Flipping}

%% Suppose we have a rule like
%% \[
%% \inferrule{\Psi'^* \vdash J_1}
%%           {\Psi' \vdash J}
%% \]
%% and we want to push a substitution $\Psi \vdash \theta : \Psi'$ into it.
%% We need to define $\flip{\Psi} \vdash \flip{\theta} : \flip{\Psi'}$,
%% i.e. the action of the opposite functor from cat to cat on morphism.
%% For the auxilary notion of terms with a variance on the right, we need
%% the corresponding principle that $\Psi \types t \vcol r A$ implies
%% $\flip{\Psi} \types \flip{t} \vcol {\flip r} A$.  

%% This is defined as follows:
%% \[
%% \begin{array}{l}
%% \flip{\cdot} = \cdot\\
%% \flip{(\theta,t/x)} = \flip{\theta},\flip{t}/x\\
%% \\
%% \flip{a} = a \text{ when $r'$ is $\ps$ or $\ms$} \\
%% \flip{(a_1,a_2)} = (a_2,a_1) \text{ when $r'$ is $\pms$} \\
%% \end{array}
%% \]

%% For the first case, we use the fact that $\flip{\uns} = \uns$.  

%% For the second, we have
%% \begin{mathpar}
%% \Psi^{v_1} \vdash \theta : \Psi' \and 
%% \Psi^{v_2} \vdash t \vcol r A  \and
%% v = {v_1} \combine v_2
%% \end{mathpar}
%% so $\flip{v} = \flip{v_1} \combine \flip{v_2}$ (FIXME: state this as a
%% lemma), and by the IH $\Psi^{\flip{v_1}} \vdash \theta : \flip{\Psi'}$,
%% and by the term lemma, $\Psi^{\flip{v_2}} \vdash t \vcol {\flip r} A$.
%% so $\flip{{\Psi^v}} \types (\flip{\theta},\flip{r}) : \flip{(\Psi', x
%%   \vcol r A)}$.

%% For terms, we use $\flip{\uns} = \uns$ in the first case, and
%% $\flip{(\flip{r})} = r$ in the $\ps$ and $\ms$ cases.  
%% For the final case, we use $\flip{v} = \flip{v_1} \combine \flip{v_2}$
%% and commutativity and involution.  

\subsection{Category Terms}

\begin{mathpar}

\inferrule{ }
          {x \pcol A \vdash x : A}

\inferrule{\Psi' \types a:A \\
            \Psi \types \rho : \Psi'
           }
           {\Psi \vdash a[\rho] :A }

\inferrule{\Psi' \types a:A \\
            \Psi \types \theta : \Psi'
           }
           {\Psi \vdash a[\theta] :A }

\begin{array}{l}
x[\rho] \equiv y \text{ if } \rho \equiv y/x\p\\
x[\theta] \equiv a \text{ if } \theta \equiv a/x\p\\
\end{array}
\end{mathpar}

\section{Type Language with Explicit Substitutions}

All of the type/context/sequent formation and term rules are in
Figure~\ref{fig:explicit}.  The definition of substitution for the
type/context/sequent rules is in Figure~\ref{fig:explicit-subst}.
Together these define provability; we still need equations for
substitutions and cuts on derivations of $\Delta \cb \Gamma \vdash M$ 
and $\beta/\eta$ etc. to define isomorphisms etc.  

\begin{figure}[p]

\begin{mathpar}

%% substitution
\inferrule{\Psi' \types J \\
            \Psi \types \rho : \Psi'
           }
           {\Psi \vdash J[\rho]}
\quad
\inferrule{\Psi' \types J \\
            \Psi \types \theta : \Psi'
           }
           {\Psi \vdash J[\theta]}
\quad
(J = \Gamma \ctx, M \type, (\Gamma \vdash M) \ok) 

%% context and sequent formation
  \inferrule{
  }{
    \ec \types \ec \ctx
  }
  \qquad
  \inferrule{
    \Psi_1 \types \Gamma \ctx\\
    \Psi_2 \types M \type\\
  }{
    {\Psi_1} \combine \Psi_2 \types \Gamma,M \ctx
  }
  \qquad
  \inferrule{
    \flip{\Psi_1} \types \Gamma \ctx\\
    {\Psi_2}\types M \type\\
  }{
    \Psi_1 \combine \Psi_2 \types (\Gamma \vdash M) \ok
  }

%% identity and substitution
\inferrule{\Phi \types N \type }
          {\Phi\complete \cb N \types N}
\qquad
\inferrule{{\Phi'}\complete  \cbb \Gamma \vdash M \\
            \Phi \types \theta : \Phi'
           }
           {\Phi\complete \cb (\Gamma \vdash M)[\flip{\theta} \combine \theta]}

%% 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{ }
          {x \mcol A \combine y\pcol A \types \mor A(x,y) \type}
\qquad
\inferrule{ }
          {z \pmcol A \cb \ec \types \mor{A}(x,y)[z/x,z/y] }
\qquad
\inferrule{%% \Psi, x \mcol A, y \pcol A \types (\Gamma \vdash M) \ok \\
           \Delta, x \pmcol A \cb (\Gamma \vdash M) [x/y\p]\\ }
          {\Delta, x \pmcol A, y \pmcol 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{
  \Psi_1 \types M_1\type \\ \Psi_2 \types M_2\type
}{
  (\Psi_1 \combine \Psi_2) \types M_1\otimes M_2\type
}
\qquad
\inferrule{
  \Delta \cb \Gamma,M_1,M_2 \types N
}{
  \Delta \cb \Gamma, M_1\otimes M_2 \types N
}
\qquad
\inferrule
    {\Phi_1 \types M_1 \type \and
      \Phi_2 \types M_2 \type
    }
    {\Phi_1\complete \combine \Phi_2\complete \cb M_1 , M_2 \types M_1 \otimes M_2}

%% coend
\inferrule{
    \Psi \combine x \pmcol A \types M \type \\
    }{
    \Psi \types \coend^{x:A} M \type
   }
\qquad
\inferrule{
  \Delta \combine x \pmcol A \cb \Gamma, M \types N
}{
  \Delta \cb \Gamma,\coend^{x:A} M \types N
}
\qquad
\inferrule{\Phi\combine x \pmcol A \vdash M \type}
          {
            \Phi\complete \combine x \pmcol A \cb M \types \coend^{x:A} M
          }

%% end
\inferrule{\Psi \combine x \pmcol A \types M \type \\
    }{
    \Psi \types \End_{x:A} M \type
  }
\qquad
\inferrule{
  \Delta \combine x \pmcol A \cb \Gamma \types M
}{
  \Delta \cb \Gamma \types \coend_{x:A} M
}
\qquad
\inferrule{\Phi \combine x \pmcol A \types M \type}
          {\Phi\complete \combine x \pmcol A \cb \End_{x:A} M \types M}

%% hom
\inferrule{
  \flip{\Psi_1} \types M_1\type \\ \Psi_2 \types M_2\type
  }{
    \Psi_1 \combine \Psi_2 \types M_1 \multimap M_2 \type
  }
\qquad
  \inferrule{
    \Delta \cb \Gamma, M \types N
  }{
    \Delta \cb \Gamma \types M\multimap N
  }
\qquad
\inferrule{
  \Phi_1 \types M_1 \type \\ 
  \Phi_2 \types M_2 \type \\ 
  }{
    \Phi_1\complete,\Phi_2\complete \cb M_1,M_1\multimap M_2 \types M_2
  }
\end{mathpar}

\caption{Explicit Substitution Calculus}
\label{fig:explicit}

\end{figure}


\begin{figure}[p]

\[
\begin{array}{rcll}
\ec [ \ec ] & \equiv & \ec \\
(\Psi_1 \vdash \Gamma, \Psi_2 \vdash M) [ \theta ] & \equiv &
\Gamma[\theta_1],M[\theta_2] & \text{ where } \theta \equiv (\theta_1 : \Psi_1, \theta_2 : \Psi_2)\\

((\Psi_1 \vdash \Gamma) \vdash (\Psi_2 \vdash M)) [ \theta ] & \equiv &
\Gamma[\flip{\theta_1}] \vdash M[{\theta_2}] & \text{ where } \theta \equiv (\theta_1 : \Psi_1, \theta_2 : \Psi_2)\\
J[\theta][\theta'] & \equiv & J[\theta[\theta']]\\

((\Psi_1 \vdash M_1) \otimes (\Psi_2 \vdash M_2)) [ \theta ] & \equiv &
M_1[\theta_1],M_2[\theta_2] & \text{ where } \theta \equiv (\theta_1 : \Psi_1, \theta_2 : \Psi_2)\\

((\Psi_1 \vdash M_1) \multimap (\Psi_2 \vdash M_2)) [ \theta ] & \equiv &
M_1[\flip{\theta_1}],M_2[\theta_2] & \text{ where } \theta \equiv (\theta_1 : \Psi_1, \theta_2 : \Psi_2)\\

(\End_{x:A} M) [ \theta ] & \equiv & \End_{x:A} M[\theta,x/x\p,x/x\m] \\

(\coend^{x:A} M) [ \theta ] & \equiv & \coend^{x:A} M[\theta,x/x\p,x/x\m]

\end{array}
\]

We also have exactly the same equations for $J[\rho]$.

\caption{Equations for Substitution}
\label{fig:explicit-subst}

\end{figure}

\clearpage
\newpage

\section{Sequent Calculus}

We write $\Delta \cbb \Gamma \types M$ to abbreviate $\Delta \vdash
(\Gamma \types M) \ok$ and $\Delta \cb \Gamma \types M$.

\begin{mathpar}
  \inferrule*[right=Hom Right Rule]{
  \Phi \types a:A
  }{
  \Phi\complete \cb \ec \types \mor{A}(a,a)
}
\end{mathpar}

Hom left rule, split into four cases (FIXME: write as single rule, without context morphism?):
\begin{mathpar}
  \inferrule*[right=Hom Left Rule-A]{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\pcol A,y\mcol A \types \Gamma' \ctx \\
    \flip{\Psi_2} \types \rho:\Psi_1' \\\\
    \Psi_2' \types M \type \\
    \Psi_3 \types a_1:A \\
    \flip{\Psi_3'} \types a_2:A \\\\
    \Psi_1,\Psi_1',\Psi_3,\Psi_3' \cb \Gamma \types \Gamma'[a_1/x\p,a_2/y\m] \\\\
    \Psi_2,\Psi_2',x\pmcol A \cb \Gamma'[\rho,x/y\m] \types M \\\\
    \unif{(\Psi_1,\Psi_3,\Psi_3') \combineU \Psi_1'}
      {\Psi_2' \combineU \Psi_2}{\rho}{(\Delta_0\types\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  }
\end{mathpar}
\begin{mathpar}
  \inferrule*[right=Hom Left Rule-B]{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\pcol A,y\mcol A \types \Gamma' \ctx \\
    \flip{\Psi_2} \types \rho:\Psi_1' \\\\
    \Psi_2' \types M \type \\
    \Psi_3 \types a_1:A \\
    \flip{\Psi_3'} \types a_2:A \\\\
    \Psi_1,\Psi_1',x\pmcol A \cb \Gamma \types \Gamma'[x/y\m] \\\\
    \Psi_2,\Psi_2',\Psi_3,\Psi_3' \cb \Gamma'[\rho,a_1/x\p,a_2/y\m] \types M \\\\
    \unif{\Psi_1 \combineU \Psi_1'}
      {(\Psi_2',\Psi_3,\Psi_3') \combineU \Psi_2}{\rho}{(\Delta_0\types\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  }
\end{mathpar}
\begin{mathpar}
  \inferrule*[right=Hom Left Rule-C]{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\pcol A \types \Gamma' \ctx \\
    \flip{\Psi_2} \types \rho:\Psi_1' \\\\
    \Psi_2' \types M \type \\
    \Psi_3 \types a_1:A \\
    \flip{\Psi_3'} \types a_2:A \\\\
    \Psi_1,\Psi_1',\Psi_3 \cb \Gamma \types \Gamma'[a_1/x\p] \\\\
    \Psi_2,\Psi_2',\Psi_3' \cb \Gamma'[\rho,a_2/x\p] \types M \\\\
    \unif{(\Psi_1,\Psi_3) \combineU \Psi_1'}
      {(\Psi_2',\Psi_3') \combineU \Psi_2}{\rho}{(\Delta_0\types\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  } \and
\end{mathpar}
\begin{mathpar}
  \inferrule*[right=Hom Left Rule-D]{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\mcol A \types \Gamma' \ctx \\
    \flip{\Psi_2} \types \rho:\Psi_1' \\\\
    \Psi_2' \types M \type \\
    \Psi_3 \types a_1:A \\
    \flip{\Psi_3'} \types a_2:A \\\\
    \Psi_1,\Psi_1',\Psi_3' \cb \Gamma \types \Gamma'[a_2/x\m] \\\\
    \Psi_2,\Psi_2',\Psi_3 \cb \Gamma'[\rho,a_1/x\m] \types M \\\\
    \unif{(\Psi_1,\Psi_3') \combineU \Psi_1'}
      {(\Psi_2',\Psi_3) \combineU \Psi_2}{\rho}{(\Delta_0\types\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  } \and
\end{mathpar}

\begin{mathpar}
\inferrule*[right=Tensor Left Rule]{
  \Delta \cb \Gamma,M_1,M_2 \types N
  }{
  \Delta \cb \Gamma, M_1\otimes M_2 \types N
}
\end{mathpar}

\begin{mathpar}
\inferrule*[right=Tensor Right Rule]{
  \Delta_1 \cbb \Gamma_1 \types M_1 \\
  \Delta_2 \cbb \Gamma_2 \types M_2
  }{
  \Delta_1, \Delta_2 \cb \Gamma_1, \Gamma_2 \types M_1 \otimes M_2
}
\end{mathpar}

\begin{mathpar}
\inferrule*[right=Coend Left Rule]{
  \Delta \combine x \pmcol A \cb \Gamma, M \types N
  }{
  \Delta \cb \Gamma,\coend^{x:A} M \types N
}
\end{mathpar}

\begin{mathpar}
\inferrule*[right=Coend Right Rule]{
  \Psi_1' \types a:A \\
  \flip{\Psi_2'} \types \rho:\Psi_1' \\\\
  \Psi_1,\Psi_2 \types (\Gamma \types \coend^{x:A} M) \ok \\\\
  \Psi_1,\Psi_1',\Psi_2,\Psi_2' \cb \Gamma \types M[a[\rho]/x\m,a/x\p] \\\\
  \unif{\Psi_1\combineU\Psi_1'}{\Psi_2\combineU\Psi_2'}{\rho}{(\Delta_0\types\rho_0)}
  }{
  \Delta_0 \cb (\Gamma \types \coend^{x:A} M)[\rho_0]
}
\end{mathpar}

\begin{mathpar}
\inferrule*[right=End Right Rule]{
  \Delta \combine x \pmcol A \cb \Gamma \types M
  }{
  \Delta \cb \Gamma \types \coend_{x:A} M
}
\end{mathpar}

\begin{mathpar}
\inferrule*[right=End Left Rule]{
  \Psi_1' \types a:A \\
  \flip{\Psi_2'} \types \rho:\Psi_1' \\\\
  \Psi_1,\Psi_2 \types (\Gamma,\End_{x:A} M \types N) \ok \\\\
  \Psi_1,\Psi_1',\Psi_2,\Psi_2' \cb \Gamma, \End_{x:A} M[a/x\m,a[\rho]/x\p] \types N \\\\
  \unif{\Psi_1\combineU\Psi_1'}{\Psi_2\combineU\Psi_2'}{\rho}{(\Delta_0\types\rho_0)}
  }{
  \Delta_0 \cb (\Gamma, \End_{x:A} M \types N)[\rho_0]
}
\end{mathpar}

\begin{mathpar}
\inferrule*[right=Arrow Right Rule]{
  \Delta \cb \Gamma, M \types N
  }{
  \Delta \cb \Gamma \types M\multimap N
}
\end{mathpar}

\begin{mathpar}
\inferrule*[right=Arrow Left Rule]{
  \Delta_1 \cbb \Gamma_1 \types M_1 \\
  \Delta_2 \cbb \Gamma_2, M_2 \types N
  }{
  \Delta_1,\Delta_2 \cb \Gamma_1,\Gamma_2,M_1\multimap M_2 \types N
}
\end{mathpar}

\subsection{Derivations}
Some of the sequent calculus rules are significantly more complicated than their explicit substitution versions.
To derive these from the simpler forms, we will need new admissible rules for unification judgements.
\begin{mathpar}
  \inferrule{
    \Delta\equiv\Delta_1,\Delta_2 \\
    \Delta_1\equiv\Psi_1,\Psi_1' \\
    \Delta_2\equiv\Psi_2,\Psi_2' \\
    \Psi_3,\Psi_3'\equiv\Psi_1,\Psi_2 \\\\
    \flip{\Psi_2'} \types \rho:\Psi_1' \\
    \Phi_1 \types \rho_1:\Psi_3' \\
    \Phi_2 \types \rho_2:\Psi_2' \\\\
    \unif{\Psi_1\combineU\Psi_1'}{\Psi_2\combineU\Psi_2'}{\rho}{(\Delta_0\types\rho_0)}
  }{
    \unif{\Psi_3\combineU(\Psi_1',\Psi_2',\Psi_3')}{\Phi_1\combineU(\Phi_2,\flip{\Phi_2},\flip{\Phi_1})}
    {(\rho[\flip{\rho_2}],\rho_2,\rho_1)}{(\Delta_0\types(1_{\Psi_3},\rho_1^{-1})[\rho_0])}
  }
\end{mathpar}

And the closely related:
\begin{mathpar}
  \inferrule{
    \Delta\equiv\Delta_1,\Delta_2 \\
    \Delta_1\equiv\Psi_1,\Psi_1' \\
    \Delta_2\equiv\Psi_2,\Psi_2' \\
    \Psi_3,\Psi_3'\equiv\Psi_1,\Psi_2 \\\\
    \flip{\Psi_2'} \types \rho:\Psi_1' \\
    \Phi_1 \types \rho_1:\Psi_3' \\
    \Phi_2 \types \rho_2:\Psi_1' \\\\
    \unif{\Psi_1\combineU\Psi_1'}{\Psi_2\combineU\Psi_2'}{\rho}{(\Delta_0\types\rho_0)}
  }{
    \unif{\Psi_3\combineU(\Psi_2',\Psi_1',\Psi_3')}{\Phi_1\combineU(\Phi_2,\flip{\Phi_2},\flip{\Phi_1})}
    {((\flip{\rho})^{-1}[\flip{\rho_2}],\rho_2,\rho_1)}{(\Delta_0\types(1_{\Psi_3},\rho_1^{-1})[\rho_0])}
  }
\end{mathpar}

\textbf{Coend:}
Recall the coend right rule:
\begin{mathpar}
\inferrule*{
  \Psi_1' \types a:A \\
  \flip{\Psi_2'} \types \rho:\Psi_1' \\\\
  \Psi_1,\Psi_2 \types (\Gamma \types \coend^{x:A} M) \ok \\\\
  \Psi_1,\Psi_1',\Psi_2,\Psi_2' \cb \Gamma \types M[a[\rho]/x\m,a/x\p] \\\\
  \unif{\Psi_1\combineU\Psi_1'}{\Psi_2\combineU\Psi_2'}{\rho}{(\Delta_0\types\rho_0)}
  }{
  \Delta_0 \cb (\Gamma \types \coend^{x:A} M)[\rho_0]
}
\end{mathpar}

To derive this in the explicit substitution calculus, first let $\Psi_3,\Psi_3'\equiv\Psi_1,\Psi_2$,
$\Psi_3\types\Gamma\ctx$, $\Psi_3',x\pmcol A\types M\type$, and let $\Phi_1\types\rho_1:\Psi_3'$ and
$\Phi_2\types\rho_2:\Psi_2'$ be renamings to (arbitrary) $\Phi$ contexts. Using the second of the
above unification rules, we can derive:
\begin{mathpar}
  \tiny
  \inferrule{
    \Delta \cb \Gamma \types M[a[\rho]/x\m,a/x\p]
    \and
    \inferrule*{
      \Phi_2\types a[\rho_2]:A
      \and
      \inferrule*{
        \inferrule{ }{
          \Phi_1\complete,x\pmcol A,y\pmcol A \cb M[\rho_1,y/x\p] \types M[\rho_1,y/x\p]
        }
      }{
        \Phi_1\complete,x\pmcol A \cb M[\rho_1] \types (\coend^{x:A}M)[\rho_1]
      }
      }{
      \Phi_1\complete,\Phi_2\complete \cb M[\rho_1,a[\flip{\rho_2}]/x\m,a[\rho_2]/x\p] \types (\coend^{x:A}M)[\rho_1]
    }
    }{
    \Delta_0 \cb (\Gamma\types\coend^{w:A}M)[\rho_0]
  }
\end{mathpar}
Moreover, it is not hard to see that this substitution and cut is completely general, making the
coend right rule the closure under substitution and cut of the corresponding explicit substitution
rule.

\textbf{Hom:}
Recall the first of the hom left rules:
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\pcol A,y\mcol A \types \Gamma' \ctx \\
    \flip{\Psi_2} \types \rho:\Psi_1' \\\\
    \Psi_2' \types M \type \\
    \Psi_3 \types a_1:A \\
    \flip{\Psi_3'} \types a_2:A \\\\
    \Psi_1,\Psi_1',\Psi_3,\Psi_3' \cb \Gamma \types \Gamma'[a_1/x\p,a_2/y\m] \\\\
    \Psi_2,\Psi_2',x\pmcol A \cb \Gamma'[\rho,x/y\m] \types M \\\\
    \unif{(\Psi_1,\Psi_3,\Psi_3') \combineU \Psi_1'}
      {\Psi_2' \combineU \Psi_2}{\rho}{(\Delta_0\types\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  }
\end{mathpar}

We will derive this from the explicit substitution rule:
\begin{mathpar}
\inferrule{
  \Delta, x \pmcol A \cb (\Gamma \vdash M) [x/y\p] \\
}{
  \Delta, x \pmcol A, y \pmcol A \cb \Gamma, \mor{A}(x,y) \types M
}
\end{mathpar}
In fact, we will only use the case where both $x$ and $y$ appear in $\Gamma$, which we rename to
$\Gamma'$ to match the hom left rule:
\begin{mathpar}
\inferrule{
  \Delta, x \pmcol A \cb \Gamma'[x/y\p] \vdash M \\
}{
  \Delta, x \pmcol A, y \pmcol A \cb \Gamma', \mor{A}(x,y) \types M
}
\end{mathpar}

We will also need another admissible unification rule:
\begin{mathpar}
\inferrule{
  \flip{\Psi_2} \types \rho:\Psi_1' \\
  \Phi_1 \types \rho_1:\Psi_3 \\
  \Phi_2 \types \rho_2:\Psi_3' \\\\
  \unif{(\Psi_1,\Psi_3,\Psi_3')\combineU\Psi_1'}{\Psi_2'\combineU\Psi_2}{\rho}{(\Delta_0\types\rho_0)}
}{
\unif{\Psi_1\combineU(\Psi_1',\Psi_3,\Psi_3')}{(\Psi_2',\Phi_1,\Phi_2)\combineU(\Psi_2,\flip{\Phi_1},\flip{\Phi_2})}
{(\rho,\rho_1,\rho_2)}{(\Delta_0\types(1_{\Psi_1},1_{\Psi_2'},\rho_1^{-1},\rho_2^{-1})[\rho_0])}
}
\end{mathpar}

We can now derive:
\begin{mathpar}
\tiny
\inferrule*{
  \Delta \cb \Gamma \types \Gamma'[a_1/x\p,a_2/y\m] \\
  \inferrule*{
    \inferrule*{}{
      \Phi_1 \types a_1[\rho_1]:A \\\\
      \flip{\Phi_2} \types a_2[\flip{\rho_2}]:A
    } \\
    \inferrule*{ 
      }{
        \Delta_2,x\pmcol A,y\pmcol A \cb \Gamma'[\rho],\mor{A}(x,y) \types M
    }
  }{
    \Delta_2,\Phi_1\complete,\Phi_2\complete \cb
    \Gamma'[\rho,a_1[\rho_1]/x\p,a_2[\rho_2]/y\m],\mor{A}(a_1[\flip{\rho_1}],a_2[\flip{\rho_2}]) \types M
  }
}{
  \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
}
\end{mathpar}

\section{Natural deduction with terms}
I think the terms for hom types are in a good form now. In a couple places I'm cheating by applying
a substitution to a sequent with term. I will fix that soon by defining an extended unification
judgement which explicitly produces substitutions to apply to terms as well as types.

With terms in the calculus, we will need a new kind of context isomorphism/renaming, which we denote
$\sigma$. Renamings $\sigma$ are only defined between $\Delta$ contexts, and effectively treat them
as ordinary contexts, ignoring the +/- resources.
\begin{mathpar}
\inferrule{ }
          {\cdot \vdash \cdot : \cdot}
\and
\inferrule{ x \pmcol A \in \Delta }
          { \Delta \vdash x/y : (y \pmcol A)}
\and
\inferrule{ \Delta_1 \vdash \sigma_1 : \Delta_1'  \\
            \Delta_2 \vdash \sigma_2 : \Delta_2' \\
           }
          { \Delta_1 \combine \Delta_2 \vdash (\sigma_1 \combine \sigma_2) : \Delta_1' \combine \Delta_2'}
\and
\inferrule{ }{ \Delta_1,\Delta_2 \types \pi_{\Delta_1}:\Delta_1 }
\end{mathpar}
(FIXME: finish/fix rules)

We also need to define an extended version of the unification judgement, which provides $\sigma$
renamings to apply to the terms involved in a cut. The judgement has the form
\[
\unif{(\Psi_1 \combineU \Psi_1')} {(\Psi_2 \combineU \Psi_2')} {\rho} {(\Delta_0 \vdash
\rho_0\cb\sigma_1\cb\sigma_2)}
\]
where the renamings $\Delta_0 \types \sigma_1:\Psi_1,\Psi_1'$ and $\Delta_0 \types
\sigma_2:\Psi_2,\Psi_2'$ are the new additions.

The rules for this extended unification judgement are
\begin{small}
\begin{mathpar}
  \inferrule{ }
            {
              \unif{(\Delta_1 \combineU \cdot)}{(\Delta_2 \combineU \cdot)}{\cdot}{({\Delta_1
              \combine \Delta_2} \vdash 1\cb\pi_{\Delta_1}\cb\pi_{\Delta_2})}
            }

  \inferrule{
    \unif{(\Psi_1 \combineU \Psi_1')}{(\Psi_2 \combineU \Psi_2')}{\rho}{(\Delta_0 \vdash \rho_0 \cb
    \sigma_1 \cb \sigma_2)}
  }{
    \unif{((\Psi_1 \combine {x \vcol {\flip v} A}) \combineU (\Psi_1' \combine {x \vcol v A}))}
         {((\Psi_2 \combine {y \vcol {v} A}) \combineU (\Psi_2' \combine {y \vcol {\flip v} A}))}
         {(\rho \combine (y/x^v))}{}
         \\\qquad
         (\Delta_0 \combine x \pmcol A \vdash \rho_0 \combine (x/x^{\flip{v}}) \combine (x/y^{v})
         \cb \sigma_1,x/x \cb \sigma_2,y/x)
  }

  \inferrule{
    [  (\Delta_2 \combine x \pmcol A \combine y \pmcol A) \equiv \Psi_2 \combine (\Psi_2' \combine x \pcol A \combine y \mcol A) ]\\\\
    ((\Delta_2 \combine x \pmcol A) \vdash (1_{\Delta_2} \combine
    x/x\m \combine x/y\p) : (\Psi_2 \combine \Psi_2')) \equiv (\Psi_3 \vdash \rho_3 : \Psi_2) \combine (\Psi_3' \vdash \rho_3' : \Psi_2')\\\\
    \unif{\Psi_1 \combineU \Psi_1'}{\Psi_3 \combineU \Psi_3'}{\rho[\flip{\rho_3'}]}
      {(\Delta_0 \vdash \rho_0 \cb \sigma_1 \cb \sigma_2,\zeta/x)}
  }{
    \unif{\Psi_1 \combineU (\Psi_1' \combine z \pmcol A)} %% {\Psi^{d_1\combine z\pm = v_1 \combine (v_1' \combine z\pm)}}
         {\Psi_2 \combineU (\Psi_2' \combine x \pcol A \combine y \mcol A)}
         {(\rho \combine x/z\m \combine y/z\p)}{} \\
         \qquad(\Delta_0 \vdash (1_{\Psi_1} \combine \rho_3)[\rho_0] \cb \sigma_1,\zeta/z \cb \sigma_2,\zeta/x,\zeta/y)
  }

  \inferrule{
    [  (\Delta_1 \combine x \pmcol A \combine y \pmcol A) \equiv \Psi_1 \combine (\Psi_1' \combine x \pcol A \combine y \mcol A) ]\\\\
    (1_{\Delta_1} \combine (x/x\m \combine x/y\p)) \equiv (\Psi_3 \vdash \rho_3 : \Psi_1 , \Psi_3' \vdash \rho_3' : \Psi_1' ) \\\\
        \unif{\Psi_3 \combineU \Psi_3'}{\Psi_2 \combineU \Psi_2'}{\rho_3'^{-1}[\rho]}
          {(\Delta_0 \vdash \rho_0 \cb \sigma_1,\zeta/x \cb \sigma_2)}
  }{
    \unif{\Psi_1 \combineU (\Psi_1' \combine x \pcol A \combine y \mcol A)}
         {\Psi_2 \combineU (\Psi_2' \combine z \pmcol A)}
         {(\rho \combine z/x\p \combine z/y\m)}{} \\
         \qquad(\Delta_0 \vdash (1_{\Psi_2} \combine \rho_3)[\rho_0] \cb \sigma_1,\zeta/x,\zeta/y \cb \zeta/z)
  }
\end{mathpar}
\end{small}

When applying a renaming to a sequent $(\Delta\cb\Gamma\types m:M)[\rho]$, the renaming applies only
to $\Gamma$ and $M$. Only $\sigma$ renamings will be applied to terms, and this will be written
$(\Delta\cb\Gamma\types m[\sigma]:M)[\rho]$. Similarly for substitutions.

Now we state the cut rule for the calculus with terms:
\begin{mathpar}
\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:M \and
            \Delta_2 \cb \Gamma_2,r:M[\rho] \vdash n:N \and
            \\\\
            \unif{\Psi_1 \combineU \Psi_1'}{\Psi_2 \combineU \Psi_2'}{\rho}{(\Delta_0 \vdash \rho_0
            \cb \sigma_1 \cb \sigma_2)} \\
           }
           {\Delta_0 \cb (\Gamma_1,\Gamma_2 \vdash n[\sigma_2,m[\sigma_1]/r]:N)[\rho_0]}
\end{mathpar}

\subsection{Hom types}
First we have identities:
\begin{mathpar}
  \inferrule{
    \Phi \types a:A
    }{
    \Phi\complete \cb \ec \types \id(a):\mor{A}(a,a)
  }
\end{mathpar}

Recall the left hom rule from the explicit substitution calculus:
\begin{mathpar}
  \inferrule{
    \Delta, x \pmcol A \cb (\Gamma \vdash M) [x/y\p] \\
    }{
    \Delta, x \pmcol A, y \pmcol A \cb \Gamma, \mor{A}(x,y) \types M
  }
\end{mathpar}
As with the sequent calculus, we will need to break this rule into cases, depending on how the
variables $x$ and $y$ break between $\Gamma$ and $M$.

The simplest case is when both variables are in $M$. First with no substitutions built in:
\begin{mathpar}
  \inferrule{
    \flip{\Psi} \types \Gamma \ctx \\
    \Psi', x\mcol A, y\pcol A \types M \type \\\\
    \Psi,\Psi', z\pmcol A \cb \Gamma \types m:M[z/x\m,z/y\p]
    }{
    \Psi,\Psi' \cb \Gamma, f:\mor{A}(x,y) \types J\pm(z.m,x,y,f):M
  }
\end{mathpar}
Building in all substitutions on the left, this becomes:
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma_1 \ctx \\
    \Psi_1', x\mcol A, y\pcol A \types M \type \\
    \flip{\Psi_2} \types \Gamma_2 \ctx \\\\
    \flip{\Psi_3} \types a_1:A \\
    \Psi_3' \types a_2:A \\\\
    \Psi_1,\Psi_1',z\pmcol A \cb \Gamma_1 \types m:M[z/x\m,z/y\p] \\
    \Psi_2,\Psi_3,\Psi_3' \cb \Gamma_2 \types f:\mor{A}(a_1,a_2)
    }{
    \Psi_1,\Psi_1',\Psi_2,\Psi_3,\Psi_3' \cb \Gamma_1,\Gamma_2 \types J\pm(z.m,a_1,a_2,f):M[a_1/x\m,a_2/y\p]
  }
\end{mathpar}
The computation rules are
\begin{gather*}
  J\pm(z.m,z,z,\id(z)) \equiv m \\
  J\pm(z.m[z/x,z/y,\id(z)/f],x,y,f) \equiv m
\end{gather*}

This can be used to define the functoriality of category terms:
\begin{mathpar}
  \inferrule{
    \Phi,x\pcol A \cb F:B \\
    \Phi_1 \types a_1:A \\
    \Phi_2 \types a_2:A
    }{
    \Phi\complete,\Phi_1\complete,\Phi_2\complete \cb f:\mor{A}(a_1,a_2) \types
    \mathtt{app}(F,f):\mor{B}(F[a_1/x\p],F[a_2/x\m])
  }
\end{mathpar}
by
\[
  \mathtt{app}(F,f) \equiv J\pm(z.\id(F),a_1,a_2,f)
\]

The next simplest case is when the variables split, with one in the domain and one in the codomain.
This gives the functoriality of types in the category variables.
With no substitutions built in, this reduces to axioms:
\begin{mathpar}
  \inferrule{
    \Phi,z\pcol A \types M \type
    }{
    \Phi\complete,x\pmcol A,y\pmcol A \cb m:M[x/z\p],f:\mor{A}(x,y) \types J\p(m,x,y,f):M[y/z\p]
  } \and
  \inferrule{
    \Phi,z\mcol A \types M \type
    }{
    \Phi\complete,x\pmcol A,y\pmcol A \cb m:M[y/z\m],f:\mor{A}(x,y) \types J\m(m,x,y,f):M[x/z\m]
  }
\end{mathpar}
And with substitutions:
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma_1 \ctx \\
    \Psi_1',z\pcol A \types M \type \\
    \flip{\Psi_2} \types \Gamma_2 \ctx \\\\
    \Psi_3 \types a_1:A \\
    \Psi_3' \types a_2:A \\
    \flip{\Psi_2'} \types \rho:\Psi_3 \\\\
    \Psi_1,\Psi_1',\Psi_3 \cb \Gamma_1 \types m:M[a_1/z\p] \\
    \Psi_2,\Psi_2',\Psi_3' \cb \Gamma_2 \types f:\mor{A}(a_1[\rho],a_2) \\\\
    \unif{(\Psi_1,\Psi_1')\combineU\Psi_3}{(\Psi_2,\Psi_3')\combineU\Psi_2'}{\rho}{(\Delta_0,\rho_0 \cb \sigma_1 \cb \sigma_2)}
    }{
    \Delta_0 \cb (\Gamma_1,\Gamma_2 \types J\p(m[\sigma_1],a_1[\sigma_1],a_2[\sigma_2],f[\sigma_2]):M[a_2/z\p])[\rho_0]
  }
\end{mathpar}
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma_1 \ctx \\
    \Psi_1',z\mcol A \types M \type \\
    \flip{\Psi_2} \types \Gamma_2 \ctx \\\\
    \flip{\Psi_3} \types a_1:A \\
    \flip{\Psi_3'} \types a_2:A \\
    \Psi_2' \types \rho:\flip{\Psi_3'} \\\\
    \Psi_1,\Psi_1',\Psi_3' \cb \Gamma_1 \types m:M[a_2/z\m] \\
    \Psi_2,\Psi_2',\Psi_3 \cb \Gamma_2 \types f:\mor{A}(a_1,a_2[\rho]) \\\\
    \unif{(\Psi_1,\Psi_1')\combineU\Psi_3'}{(\Psi_2,\Psi_3)\combineU\Psi_2'}{\flip{\rho}}{(\Delta_0,\rho_0
    \cb \sigma_1 \cb \sigma_2)}
    }{
    \Delta_0 \cb (\Gamma_1,\Gamma_2 \types J\m(m[\sigma_1],a_1[\sigma_2],a_2[\sigma_1],f[\sigma_2]):M[a_1/z\m])[\rho_0]
  }
\end{mathpar}
These have computation rules
\begin{gather*}
  J\p(m,a,a,\id(a)) \equiv m \\
  J\p(m[z/x,z/y,\id(z)],x,y,f) \equiv m \\
  J\m(m,a,a,\id(a)) \equiv m \\
  J\m(m[z/x,z/y,\id(z)],x,y,f) \equiv m
\end{gather*}

The most complicated case is when both variables appear in $\Gamma$.
This further splits into two cases, depending on whether the $x$ and $y$ in $\Gamma$ appear in the same or in different types.
Without substitutions built in, we have
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \flip{\Psi_2}, x\pcol A \types N_1 \type \\
    \flip{\Psi_3}, y\mcol A \types N_2 \type \\
    \Psi' \types M \type \\\\
    \Delta \equiv \Psi_1,\Psi_2,\Psi_3,\Psi' \\
    \Delta,z\pmcol A \cb \Gamma, r:N_1[z/x\p], s:N_2[z/y\m] \types m:M
    }{
    \Delta,x\pmcol A,y\pmcol A \cb \Gamma, r':N_1, s':N_2, f:\mor{A}(x,y) \types \\\\
      \quad(\transa{r}{r'}{x}{s}{s'}{y}{z}{f}{m}):M
  }
\end{mathpar}
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \flip{\Psi_2}, x\pcol A, y\mcol A \types N \type \\
    \Psi' \types M \type \\\\
    \Delta \equiv \Psi_1,\Psi_2,\Psi' \\
    \Delta,z\pmcol A \cb \Gamma, r:N[z/x\p,z/y\m] \types m:M
    }{
    \Delta,x\pmcol A,y\pmcol A \cb \Gamma, r':N, f:\mor{A}(x,y) \types \\\\
      \quad(\transb{r}{r'}{x}{y}{z}{f}{m}):M
  }
\end{mathpar}

With substitutions, these become
\begin{mathpar}
  \inferrule{
    \flip{\Psi_{11}} \types \Gamma_1 \ctx \\
    \flip{\Psi_{12}} \types \Gamma_2 \ctx \\
    \flip{\Psi_{23}} \types \Gamma_3 \ctx \\\\
    \Psi_{11}', x\pcol A \types N_1 \type \\
    \Psi_{12}', y\mcol A \types N_2 \type \\
    \Psi_2' \types M \type \\\\
    \Psi_3 \types a_1:A \\
    \flip{\Psi_3'} \types a_2:A \\
    \flip{\Psi_{21}} \types \rho_1:\Psi_{11}' \\
    \flip{\Psi_{22}} \types \rho_2:\Psi_{12}' \\\\
    \Psi_{11},\Psi_{11}',\Psi_3 \cb \Gamma_1 \types n_1:N_1[a_1/x\p] \\
    \Psi_{12},\Psi_{12}',\Psi_3' \cb \Gamma_2 \types n_2:N_2[a_2/y\m] \\\\
    \Psi_{21},\Psi_{22},\Psi_{23},\Psi_2',x\pmcol A
      \cb \Gamma_3, r:N_1[\rho_1], s:N_2[\rho_2,x/y\m] \types m:M \\\\
    \unif{(\Psi_{11},\Psi_3,\Psi_{12},\Psi_3')\combineU(\Psi_{11}',\Psi_{12}')}
      {(\Psi_{23},\Psi_2')\combineU(\Psi_{21},\Psi_{22})}{(\rho_1,\rho_2)}{(\Delta_0\types\rho_0 \cb
      \sigma_1 \cb \sigma_2)}
    }{
    \Delta_0 \cb (\Gamma_1,\Gamma_2,\Gamma_3,f:\mor{A}(a_1,a_2) \types \\
      \quad(\transa{r}{n_1[\sigma_1]}{a_1[\sigma_1]}{s}{n_2[\sigma_1]}{a_2[\sigma_1]}{x}{f}{m[\sigma_2]}):M)[\rho_0]
  }
\end{mathpar}
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma_1 \ctx \\
    \flip{\Psi_{22}} \types \Gamma_2 \ctx \\
    \Psi_1', x\pcol A, y\mcol A \types N \type \\
    \Psi_2' \types M \type \\\\
    \Psi_3 \types a_1:A \\
    \flip{\Psi_3'} \types a_2:A \\
    \flip{\Psi_{21}} \types \rho:\Psi_1' \\\\
    \Psi_1,\Psi_1',\Psi_3,\Psi_3' \cb \Gamma_1 \types n:N[a_1/x\p,a_2/y\m] \\\\
    \Psi_{21},\Psi_{22},\Psi_2',x\pmcol A
      \cb \Gamma_2, r:N[\rho,x/y\m] \types m:M \\\\
    \unif{(\Psi_1,\Psi_3)\combineU\Psi_1'}
      {(\Psi_{22},\Psi_2')\combineU\Psi_{21}}{\rho}{(\Delta_0\types\rho_0 \cb \sigma_1 \cb \sigma_2)}
    }{
    \Delta_0 \cb (\Gamma_1,\Gamma_2,\Gamma_3,f:\mor{A}(a_1,a_2) \types \\
    \quad(\transb{r}{n[\sigma_1]}{a_1[\sigma_1]}{a_2[\sigma_1]}{x}{f}{m[\sigma_2]}):M)[\rho_0]
  }
\end{mathpar}

The computation rules for these terms are
\begin{gather*}
  (\transa{r}{n_1}{a}{s}{n_2}{a}{x}{\id(a)}{m}) \equiv m[a/x,n_1/r,n_2/s] \\
  (\transa{r}{r}{x}{s}{s}{y}{z}{f}{m[z/x,z/y,\id(z)/f]}) \equiv m \\
  (\transb{r}{n}{a}{a}{x}{\id(a)}{m}) \equiv m[a/x,n/r] \\
  (\transb{r}{r}{x}{y}{z}{f}{m[z/x,z/y,\id(z)/f]}) \equiv m
\end{gather*}

\subsection{Coend}
\begin{mathpar}
\inferrule{
  \Delta \combine x \pmcol A \cb \Gamma, r:M \types n:N
}{
  \Delta \cb \Gamma,s:\coend^{x:A} M \types \clet x,r:=s in n:N
}
\qquad
\inferrule{\Phi\combine x \pmcol A \vdash M \type}
          {
            \Phi\complete \combine x \pmcol A \cb r:M \types \cpair{x}{r}:\coend^{x:A} M
          }
\end{mathpar}
and with substitutions:
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma_1 \ctx \\
    \flip{\Psi_{21}} \types \Gamma_2 \ctx \\
    \Psi_1',x\pmcol A \types M \type \\
    \Psi_2' \types N \type \\\\
    \flip{\Psi_{22}} \types \rho:\Psi_1' \\
    \Psi_1,\Psi_1' \cb \Gamma_1 \types m:\coend^{x:A} M \\\\
    \Psi_{21},\Psi_{22},\Psi_2',z\pmcol A \cb \Gamma_2, r:M[\rho,z/x\p,z/x\m] \types n:N \\\\
    \unif{\Psi_1\combineU\Psi_1'}{(\Psi_{21},\Psi_2')\combineU\Psi_{22}}{\rho}{(\Delta_0\types\rho_0\cb\sigma_1\cb\sigma_2)}
    }{
    \Delta_0 \cb (\Gamma_1,\Gamma_2 \types \clet z,r:=m[\sigma_1] in n[\sigma_2]:N)[\rho_0]
  }
  \and
  \inferrule{
    \Psi_1' \types a:A \\
    \flip{\Psi_2'} \types \rho:\Psi_1' \\\\
    \Psi_1,\Psi_2 \types (\Gamma \types \coend^{x:A} M) \ok \\\\
    \Psi_1,\Psi_1',\Psi_2,\Psi_2' \cb \Gamma \types m:M[a[\rho]/x\m,a/x\p] \\
    \unif{\Psi_1\combineU\Psi_1'}{\Psi_2\combineU\Psi_2'}{\rho}{(\Delta_0\types\rho_0\cb\sigma_1\cb\sigma_2)}
    }{
    \Delta_0 \cb (\Gamma \types \cpair{a[\sigma_1]}{m[\sigma_1,\sigma_2]}:\coend^{x:A} M)[\rho_0]
  }
\end{mathpar}

The computation rules are
\begin{gather*}
  (\clet z,r:=\cpair{a}{m} in n) \equiv n[a/z,m/r] \\
  (\clet x,r:=s in n[\cpair{x}{r}/z]) \equiv n[s/z]
\end{gather*}

\subsection{Arrow types}
Without substitutions:
\begin{mathpar}
  \inferrule{
    \Delta \cb \Gamma, r:M \types n:N
  }{
    \Delta \cb \Gamma \types \lambda r.n:M\multimap N
  } \and
  \inferrule{
    \Phi_1 \types M_1 \type \\
    \Phi_2 \types M_2 \type \\
  }{
    \Phi_1\complete,\Phi_2\complete \cb r:M_1,s:M_1\multimap M_2 \types sr:M_2
  }
\end{mathpar}
The second, with substitutions, becomes
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma_1 \ctx \\
    \flip{\Psi_2} \types \Gamma_2 \ctx \\
    \Psi_1' \types M \type \\
    \Psi_{22}' \types N \type \\\\
    \flip{\Psi_{21}'} \types \rho:\Psi_1' \\
    \Psi_1,\Psi_1' \cb \Gamma_1 \types m:M \\
    \Psi_2,\Psi_{21}',\Psi_{22}' \cb \Gamma_2 \types t:M[\rho]\multimap N \\\\
    \unif{\Psi_1\combineU\Psi_1'}{(\Psi_2,\Psi_{22}')\combineU\Psi_{21}'}{\rho}{(\Delta_0\types\rho_0\cb\sigma_1\cb\sigma_2)}
    }{
    \Delta_0 \cb (\Gamma_1,\Gamma_2 \types t[\sigma_2]m[\sigma_1]:N)[\rho_0]
  }
\end{mathpar}
The computation rules are
\begin{gather*}
  (\lambda r.n)s \equiv n[s/r] \\
  \lambda r.(sr) \equiv s
\end{gather*}
\end{document}