resource3.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}
\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 $\Delta_1 \cb \Phi \cb \Delta_2 \cb \Gamma \vdash M$, presupposes 
  $\Delta_1,\Phi \types \Gamma \ctx$
  and 
  $\Phi,\Delta_2 \types M \type$
  
\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) 

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

%% identity and substitution
\inferrule{\Phi \types N \type }
          {\cdot \cb \Phi \cb \cdot \cb N \types N}
\qquad
\inferrule{\Phi_1 \types \theta : \Phi_1' \and
           \Phi \types \theta : \Phi' \and
           \Phi_2 \types \theta : \Phi_2' \and
           {\Phi_1'}\complete \cb \Phi' \cb {\Phi_2'}\complete \cbb \Gamma \types M
           }
           {\Phi_1\complete \cb \Phi \cb \Phi_2\complete \cb \Gamma[\flip{\theta_1},\theta_1,\theta] \vdash M[\flip{\theta_2},\theta_2,\theta]}

%% cut
%% TODO
%% \inferrule{ (\Delta_1 \combine \Delta_2) \ctx \and
%%             \Delta_1 = \Psi_1 \combine \Psi_1' \and
%%             \Delta_2 = \Psi_2 \combine \Psi_2' \\\\
%%             \Psi_1' \types M \type \and
%%             \flip{\Psi_2'} \types \rho : \Psi_1' \and
%%             \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 \combine \Psi_1'}{\Psi_2 \combine \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{ }
          {\cdot \cb \cdot \cb x \pmcol A \cb \ec \types \mor{A}(x,x) }
\qquad
\\
\inferrule{\ldots}
          {\Delta_1, x \pmcol A, y \pmcol A \cb \Phi \cb \Delta_2 \cb \Gamma, \mor{A}(x,y) \types M }
\qquad
\inferrule{\ldots}
          {\Delta_1 \cb \Phi, x \pmcol A, y \pmcol A \cb \Delta_2 \cb \Gamma, \mor{A}(x,y) \types M }
\\
\inferrule{\ldots} %% {\Delta, x \pmcol A \cb (\Gamma \vdash M) [x/y\p]\\ }
          {\Delta_1,x \pmcol A \cb \Phi, y \pcol A \cb \Delta_2 \cb \Gamma, \mor{A}(x,y) \types M }
\qquad
\inferrule{\ldots}
          {\Delta_1, y \pmcol A \cb \Phi, x \mcol A \cb \Delta_2 \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_1 \cb \Phi \cb \Delta_2 \cb \Gamma,M_1,M_2 \types N
}{
  \Delta_1 \cb \Phi \cb \Delta_2 \cb \Gamma, M_1\otimes M_2 \types N
}
\qquad
\inferrule
    {\Phi_1 \types M_1 \type \and
      \Phi_2 \types M_2 \type
    }
    {\cdot \cb \Phi_1,\Phi_2 \cb \cdot \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_1\combine x \pmcol A \cb \Phi \cb \Delta_2 \cb \Gamma, M \types N
}{
  \Delta_1 \cb \Phi \cb \Delta_2 \cb \Gamma,\coend^{x:A} M \types N
}
\qquad
\inferrule{\Phi\combine x \pmcol A \vdash M \type}
          {
            x \pmcol A \cb \Phi \cb \cdot \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_1 \cb \Phi \cb \Delta_2 \combine x \pmcol A \cb \Gamma \types M
}{
  \Delta_1 \cb \Phi \cb \Delta_2 \cb \Gamma \types \coend_{x:A} M
}
\qquad
\inferrule{\Phi \combine x \pmcol A \types M \type}
          {\cdot \cb \Phi \cb  x \pmcol A \cb \End_{x:A} M \types M}

%% arrow
\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{
    \text{move some stuff left} \cb \Gamma, M \types N
  }{
    \Delta_1 \cb \Phi \cb \Delta_2 \cb \Gamma \types M\multimap N
  }
\qquad
\inferrule{
  \Phi_1 \types M_1 \type \\ 
  \Phi_2 \types M_2 \type \\ 
  }{
    \Phi_1\pm \cb \Phi_2 \cb \cdot \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$.

Hom right rule:
\begin{mathpar}
  \inferrule{
    \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{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\pcol A,y\mcol A \types \Gamma' \ctx \\
    \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 \\\\
    \flip{\Psi_2} \types \rho:\Psi_1' \\
    \unif{(\Psi_1,\Psi_3,\Psi_3') \combineU \Psi_1'}
      {\Psi_2' \combineU \Psi_2}{\rho}{(\Delta_0,\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  }
\end{mathpar}
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\pcol A,y\mcol A \types \Gamma' \ctx \\
    \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 \\\\
    \flip{\Psi_2} \types \rho:\Psi_1' \\
    \unif{\Psi_1 \combineU \Psi_1'}
      {(\Psi_2',\Psi_3,\Psi_3') \combineU \Psi_2}{\rho}{(\Delta_0,\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  }
\end{mathpar}
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\pcol A \types \Gamma' \ctx \\
    \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 \\\\
    \flip{\Psi_2} \types \rho:\Psi_1' \\
    \unif{(\Psi_1,\Psi_3) \combineU \Psi_1'}
      {(\Psi_2',\Psi_3') \combineU \Psi_2}{\rho}{(\Delta_0,\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  } \and
\end{mathpar}
\begin{mathpar}
  \inferrule{
    \flip{\Psi_1} \types \Gamma \ctx \\
    \Psi_1',x\mcol A \types \Gamma' \ctx \\
    \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 \\\\
    \flip{\Psi_2} \types \rho:\Psi_1' \\
    \unif{(\Psi_1,\Psi_3') \combineU \Psi_1'}
      {(\Psi_2',\Psi_3) \combineU \Psi_2}{\rho}{(\Delta_0,\rho_0)}
    }{
    \Delta_0 \cb (\Gamma,\mor{A}(a_1,a_2) \types M)[\rho_0]
  } \and
\end{mathpar}

Tensor left rule:
\begin{mathpar}
\inferrule{
  \Delta \cb \Gamma,M_1,M_2 \types N
}{
  \Delta \cb \Gamma, M_1\otimes M_2 \types N
}
\end{mathpar}

Tensor right rule:
\begin{mathpar}
\inferrule{
  \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}

Coend left rule:
\begin{mathpar}
\inferrule{
  \Delta \combine x \pmcol A \cb \Gamma, M \types N
  }{
  \Delta \cb \Gamma,\coend^{x:A} M \types N
}
\end{mathpar}

Coend right rule:
\begin{mathpar}
\inferrule{
  \Psi_1,\Psi_2 \types (\Gamma \types \coend^{x:A} M) \ok \\
  \Psi_1' \types a:A \\
  \flip{\Psi_2'} \types \rho:\Psi_1' \\\\
  \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,\rho_0)}
  }{
  \Delta_0 \cb (\Gamma \types \coend^{x:A} M)[\rho_0]
}
\end{mathpar}

End right rule:
\begin{mathpar}
\inferrule{
  \Delta \combine x \pmcol A \cb \Gamma \types M
  }{
  \Delta \cb \Gamma \types \coend_{x:A} M
}
\end{mathpar}

End left rule:
\begin{mathpar}
\inferrule{
  \Psi_1,\Psi_2 \types (\Gamma,\End_{x:A} M \types N) \ok \\
  \Psi_1' \types a:A \\
  \flip{\Psi_2'} \types \rho:\Psi_1' \\\\
  \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,\rho_0)}
  }{
  \Delta_0 \cb (\Gamma, \End_{x:A} M \types N)[\rho_0]
}
\end{mathpar}

Arrow right rule:
\begin{mathpar}
\inferrule{
  \Delta \cb \Gamma, M \types N
  }{
  \Delta \cb \Gamma \types M\multimap N
}
\end{mathpar}

Arrow left rule:
\begin{mathpar}
\inferrule{
  \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}
\end{document}