resource4.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{\Ja}[9]{\mathtt{transport}\; #1\coloneqq #2@#3 \;\mathtt{and}\; #4\coloneqq #5@#6
  \;\mathtt{to}\; #7 \;\mathtt{via}\; #8 \;\mathtt{in}\; #9}
\newcommand{\Jb}[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}
\Psi ::= \cdot \mid \Psi_1,\Psi_2 \mid x : A \\
\\ 
\Gamma ::= \cdot \mid \Gamma, M\\
\end{array}
\end{mathpar}

Judgements:

\begin{itemize}

\item $\Psi' \cb \Psi \types a : A$

\item $\Psi' \cb \Psi \types M \type$

\item $\Psi' \cb \Psi \types \Gamma \ctx$

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

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

\end{itemize}

\section{Category Language with Explicit Substitutions}

\subsection{Category Contexts}

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

\inferrule{ }{(x : A) \ctx}

\inferrule{ \Psi_1 \ctx \and \Psi_2 \ctx \and (\text{variables are distinct})\\
          }
          {\Psi_1 \combine \Psi_2 \ctx}
\end{mathpar}

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}

All future judgements are defined on equivalence classes of contexts.  

\subsection{Context Isomorphisms}

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

\begin{mathpar}
\inferrule{ }
          {\cdot \vdash \cdot : \cdot}
\and
\inferrule{ }
          { x : A \vdash x/y : y : 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}
\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 the groupoid/involution laws:
\begin{mathpar}
\begin{array}{rcl}
1_\cdot & \equiv & \cdot \\
1_{x : A} & \equiv & x/x\\
1_{\Psi_1,\Psi_2} & \equiv & 1_{\Psi_1},1_{\Psi_2}\\
\end{array}
\quad
\begin{array}{rcl}
\cdot^{-1} & \equiv & \cdot\\
(x/y)^{-1} & \equiv & y/x\\
(\rho_1,\rho_2)^{-1} & \equiv & \rho_1^{-1},\rho_2^{-1}\\
\end{array}

\begin{array}{rcll}
\cdot[\rho'] & \equiv & \cdot \\
(x/y)[\rho'] & \equiv & z/y & \text{ if } \rho \equiv z/x \\
(\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 \\
\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$ from $\rho$ for $x : A \in \Psi_1$ and $\rho_2$
contains all bindings $y/x$ from $\rho$ for $x : A \in \Psi_2$;
we could also write this out formally as an operation on trees.

\subsection{Unification of Renamings}

(not ported yet)


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

FIXME: could also force the $\cb$ split first?  This is the
substitutions for resource2 with the new type system; I haven't thought
about whether this is the nicest way to do things yet.  

\begin{mathpar}
\inferrule{ }
          {\cdot \cb \cdot \vdash \cdot : \cdot \cb \cdot}
\and
\inferrule{ \Psi' \cb \Psi \vdash a : A}
          { \Psi' \cb \Psi \vdash a/x\p : \cdot \cb x : A}
\and
\inferrule{ \Psi \cb \Psi' \vdash a : A}
          { \Psi' \cb \Psi \vdash a/x\m : x : A \cb \cdot}
\and 
\inferrule{ \Psi_1' \cb \Psi_1 \vdash \theta_2 : \Psi_2' \cb \Psi_2  \\
            \Psi_3' \cb \Psi_3 \vdash \theta_4 : \Psi_4' \cb \Psi_4 \\
           }
          { \Psi_1',\Psi_3' \cb \Psi_1,\Psi_3 \vdash (\theta_2 \combine \theta_4) : \Psi_2',\Psi_4' \cb \Psi_2,\Psi_4}
\\\\
\inferrule{ }
          {\Psi' \cb \Psi \vdash 1 : \Psi' \cb \Psi }
\and
\inferrule{\Psi' \cb \Psi \vdash \theta_1 : \Psi_1' \cb \Psi_1 \and
           \Psi_1' \cb \Psi_1 \vdash \theta_2 : \Psi_2' \cb \Psi_2}
          {\Psi' \cb \Psi \vdash \theta_2[\theta_1] : \Psi_2' \cb \Psi_2 }
\and 
\inferrule{\Psi' \cb \Psi \vdash \theta : \Psi_1' \cb \Psi_1}
          {\Psi \cb \Psi' \vdash \flip{\theta} : {\Psi_1} \cb \Psi_1' }
\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{ }
          {\cdot \cb x : A \vdash x : A}

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

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

\begin{array}{l}
x[\rho_1 \cb \rho_2] \equiv y \text{ if } \rho_1 \equiv \cdot \text{ and} \rho_2 \equiv y/x\\
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_1' \cb \Psi_2' \types J \\
            \Psi_1 \types \rho_1 : \Psi_1' \\
            \Psi_2 \types \rho_2 : \Psi_2'
           }
           {\Psi_1 \cb \Psi_2 \vdash J[\rho_1 \cb \rho_2]}
\quad
\inferrule{\Psi_1' \cb \Psi_2' \types J \\
            \Psi_1 \cb \Psi_2 \types \theta : \Psi_1' \cb \Psi_2'
           }
           {\Psi \vdash J[\theta]}
\\
(J = \Gamma \ctx, M \type, (\Gamma \vdash M) \ok) 

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

%% identity and substitution
\inferrule{\Psi' \cb \Psi \types N \type }
          {\Psi',\Psi \cb N \types N}
\qquad
\inferrule{ \Psi_1',\Psi_1  \cbb \Gamma \vdash M \\
            \Psi_2' \cb \Psi_2 \types \theta : \Psi_1' \cb \Psi_1
           }
           {\Psi_2',\Psi_2 \cb (\Gamma \vdash M)[\flip{\theta}, \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 : A \cb y : A \types \mor A(x,y) \type}
\qquad
\inferrule{ }
          {x : A \cb \ec \types \mor{A}(x,x) }
\qquad
\inferrule{\Psi, x : A \cb (\Gamma \vdash M) [1_\Psi,x/x \cb 1_\Psi,x/y]\\ }
          {\Psi, x : A, 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{
  \Psi_1' \cb \Psi_1 \types M_1\type \\ \Psi_2' \cb \Psi_2 \types M_2\type
}{
  \Psi_1',\Psi_2' \cb \Psi_1,\Psi_2 \types M_1\otimes M_2\type
}
\qquad
\inferrule{
  \Psi \cb \Gamma,M_1,M_2 \types N
}{
  \Psi \cb \Gamma, M_1\otimes M_2 \types N
}
\\
\inferrule
    {\Psi_1' \cb \Psi_1 \types M_1 \type \and
     \Psi_2' \cb \Psi_2 \types M_2 \type
    }
    {\Psi_1,\Psi_1',\Psi_2,\Psi_2' \cb M_1 , M_2 \types M_1 \otimes M_2}

%% coend
\inferrule{
    \Psi',x:A \cb \Psi,x:A \types M \type \\
    }{
    \Psi' \cb \Psi \types \coend^{x:A} M \type
   }
\qquad
\inferrule{
  \Psi, x : A \cb \Gamma, M \types N
}{
  \Psi \cb \Gamma,\coend^{x:A} M \types N
}
\qquad
\inferrule{\Psi', x : A \cb \Psi,x : A \vdash M \type}
          {
            \Psi',\Psi, x : A \cb M \types \coend^{x:A} M
          }

%% end
\inferrule{\Psi', x : A \cb \Psi, x : A \types M \type \\
    }{
    \Psi' \cb \Psi \types \End_{x:A} M \type
  }
\qquad
\inferrule{
  \Psi', x : A \cb \Gamma \types M
}{
  \Psi \cb \Gamma \types \coend_{x:A} M
}
\qquad
\inferrule{\Psi', x : A \cb \Psi, x : A \types M \type}
          {\Psi',\Psi, x : A \cb \End_{x:A} M \types M}

%% arrow
\inferrule{
  {\Psi_1} \cb \Psi_1' \types M_1\type \\ 
  \Psi_2' \cb \Psi_1 \types M_2\type
  }{
    \Psi_1',\Psi_2' \cb \Psi_1,\Psi_2 \types M_1 \multimap M_2 \type
  }
\qquad
  \inferrule{
    \Psi \cb \Gamma, M \types N
  }{
    \Psi \cb \Gamma \types M\multimap N
  }
\qquad
\inferrule{
  \Psi_1 \cb \Psi_1' \types M_1 \type \\ 
  \Psi_2' \cb \Psi_2 \types M_2 \type \\ 
  }{
    \Psi_1',\Psi_1,\Psi_2',\Psi_2 \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
\end{document}

\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{Term calculus}
Starting to play with terms again, with some new ideas. Feel free to ignore for now\dots

\subsection{Hom types}
We seem to need several special cases for elim terms for hom types. To begin with, the \textsc{Hom
Left Rule-A} splits into two cases, depending on whether the $x$ and $y$ in $\Gamma'$ appear in the
same or in different types.
\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)}
    }{
    \Delta_0 \cb (\Gamma_1,\Gamma_2,\Gamma_3,f:\mor{A}(a_1,a_2)
      \types (\Ja{r}{n_1}{a_1}{s}{n_2}{a_2}{x}{f}{m}):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 \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)}
    }{
    \Delta_0 \cb (\Gamma_1,\Gamma_2,\Gamma_3,f:\mor{A}(a_1,a_2)
      \types (\Jb{r}{n}{a_1}{a_2}{x}{f}{m}):M)[\rho_0]
  }
\end{mathpar}

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