\nonstopmode
\documentclass[fleqn,a4paper]{article}
\usepackage{fullpage}
\usepackage{xspace}
\usepackage{ifthen}
\usepackage{amsmath}
\usepackage{amssymb}
%\usepackage{amsthm}
\usepackage{stmaryrd}
\usepackage{graphicx}
%\usepackage[all]{xy}
%\usepackage{txfonts} % dont like the look of it!
%\usepackage{upgreek} \newcommand{\omegaup}{\upomega}
%\usepackage{mathabx}

% more vertical spacing in array
\usepackage{tabularx}
\setlength{\extrarowheight}{1pt}

\usepackage[usenames,dvipsnames]{color}
\usepackage{hyperref}
\hypersetup{colorlinks=true, linkcolor=Red, citecolor=ForestGreen, urlcolor=RoyalBlue}
%\usepackage[hyperindex, dvipdfm]{hyperref}
%\makeindex

% DESTROYS HORIZONTAL ALIGNMENT of super/sub
% % allow double superscripts
% \catcode`\^ = 13 \def^#1{\sp{#1}{}}
% \catcode`\_ = 13 \def_#1{\sb{#1}{}}

% More space for floats
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
\renewcommand{\floatpagefraction}{0.90}
\renewcommand{\textfraction}{0.1}

% \newtheorem{deflem}[theorem]{Def. and Lem.}

\ifdefined\LONGVERSION
  \relax
\else
% short version:
\newcommand{\LONGVERSION}[1]{}
\newcommand{\SHORTVERSION}[1]{#1}
% % long version:
% \newcommand{\LONGVERSION}[1]{#1}
% \newcommand{\SHORTVERSION}[1]{}
% \newcommand{\SHORTVERSION}[1]{BEGIN~SHORT\ #1 \ END~SHORT}
\fi
\newcommand{\LONGSHORT}[2]{\LONGVERSION{#1}\SHORTVERSION{#2}}

\newtheorem{theorem}{Theorem}
\newtheorem{proposition}{Proposition}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{conjecture}{Conjecture}
\newtheorem{definition}{Definition}
\newtheorem{remark}{Remark}
\newtheorem{example}{Example}

\def\theoremautorefname{Theorem}
\def\lemmaautorefname{Lemma}

%\newcommand{\qed}{\hfill\ensuremath{\Box}}
% from llncs.cls
%\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\def\squareforqed{\ensuremath{\Box}}
\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

\newenvironment{proof}[1][]{\noindent\ifthenelse{\equal{#1}{}}{{\it
      Proof.}}{{\it Proof #1.}}\hspace{2ex}}{\qed\bigskip}
\newenvironment{proof*}[1][]{\noindent\ifthenelse{\equal{#1}{}}{{\it
      Proof.}}{{\it Proof #1.}}\hspace{2ex}}{\bigskip}

\input{prooftree}
\newcommand{\inst}{}
\input{macros}

\setlength{\parindent}{0ex}
\setlength{\parskip}{0.3em}

\title{Shape-Irrelevant Dependent Types and Unification Constraints \\
Or: \\
Why Pattern Inductive Families Need Not Store Their Indices}
\author{Andreas Abel, Christoph-Simon Senjak}
\date{December 2012}

\begin{document}
\maketitle

\nocite{abelScherer:types10}

TODO.
\begin{enumerate}
\item map and foldr for RVec and IVec
\item Write typing rules
\end{enumerate}

\section{Syntax}

Grammar.
\[
\begin{array}{@{}lllrll}
  \Ann & \ni & \evar & ::= & \noterased & \mbox{relevant} \\ 
    &&& \mid & \nonstrict & \mbox{shape-irrelevant} \\
    &&& \mid & \erased & \mbox{irrelevant} \\[1em]
  \Exp & \ni & r,s,t,u, \\ && S,T, U & ::= & 
   % 0 \mid  empty type is definable via unsolvable unification constraint
   1 & \mbox{unit type} \\
   &&& \mid & () & \mbox{unit intro} \\
   &&& \mid & r \noterasedeq s \mid r \nonstricteq s \mid r \erasedeq s & \mbox{intensional equalities} \\
  &&& \mid & T_1 + T_2 & \mbox{disjoint sum} \\
   &&& \mid & \inl t \mid \inr t \mid \caseof[T] r s t 
    & \mbox{disjoint sum intro/elim} \\
  &&& \mid & \efunT x U T & \mbox{dependent function type} \\
   &&& \mid & x \mid \lambda x t \mid r\,s 
    & \mbox{lambda-calculus} \\
  &&& \mid & \esigT x U T & \mbox{dependent pair type} \\
%%  &&& \mid & (t_1,t_2) \mid \fst r \mid \snd r & \mbox{pair intro/elim} \\
  &&& \mid & (t_1,t_2) \mid \unpair[T] t f & \mbox{pair intro/elim} \\
  &&& \mid & \mu T & \mbox{inductive type} \\
   &&& \mid & \tin\,t \mid \tout\,r \mid \rec[T] t
    & \mbox{inductive type intro/elim} \\
  &&& \mid & \unifT \Delta p t T U  & \mbox{unification constraint}\\
%  &&& \mid & \unif u p T  & \mbox{unification constraint}\\
%     \mid \Eq[T] t {t'}
   &&& \mid & \splitno r & \mbox{empty type elimination} \\
   &&& \mid & \splitin r {\hat\Delta} x t & \mbox{constraint elimination} \\ 
  &&& \mid & \Set  & \mbox{universe of small types} \\[1em]
  \Cxt   & \ni & \Gamma,\Delta & ::= & \cempty \mid \eext \Gamma x T
    & \mbox{contexts} \\
  \Pat & \ni & p,q & ::= & x \mid \inl p \mid \inr p \mid (p_1,p_2)
  \mid \tin\,p 
  & \mbox{patterns} \\
  \UP & \ni & P,Q  & ::= & \unifP \Delta p t T
  & \mbox{unification problem} \\
\end{array}
\]

We let $\cdom\Delta$ denote the list of the variables bound in
$\Delta$.  Thus, $\cdom\cempty = \cempty$ and 
$\cdom{\eext \Delta x T} = \cdom\Delta, x$.  The variables $\cdom P$
bound by a unification problem are $\cdom{\unifP \Delta p t T} = \cdom\Delta$. 
Further, let $\FV(t)$ be the list of free variable occurrences in term
$t$.


\para{Substitutions} $\sigma$ are maps from variables to
expressions.  We require that the domain $\dom(\sigma) = \{ x \mid
\sigma(x) \not= x \}$ is finite.  We write $\sid$ for the identity
substitution and $\subst u x {}$ for the singleton substitution
$\sigma$ with $\dom(\sigma) = \{ x\}$ and $\sigma(x) = u$.  Capture
avoiding parallel substitution of $\sigma$ in $t$ is written as
juxtaposition $t \sigma$.



\para{Operations on relevance annotations and contexts} Let the linear 
order \emph{more irrelevant} $\leq$ on relevance annotations be given
by $\noterased \leq \nonstrict \leq \erased$.
Relevance composition is given by:
\[
  \evar_1 \evar_2 = \max(\evar_1,\evar_2)
\]
Relevance ``exponentiation''.
\[
\begin{array}{llll}
  \resurrect\erased & = & \nonstrict \\
  \resurrect\evar   & = & \evar & \mfor \evar \not= \erased \\
\end{array}
\qquad
\begin{array}{llll}
  \resurrect[\ominus]\nonstrict & = & \erased \\
  \resurrect[\ominus]\evar   & = & \evar & \mfor \evar \not= \nonstrict \\
\end{array}
\qquad
\begin{array}{llll}
  \resurrect[\evar_2]{\evar_1} & = & \left\{
    \begin{array}{ll}
      \noterased & \mif \evar_1 \leq \evar_2 \\
      \evar_1    & \motherwise
    \end{array}
  \right.
\end{array}
\]
These operations are idempotent. 
$\resurrect-$ and $\resurrect[-]{\evar_0}$ are antitone,
$\resurrect[\ominus]{-}$ and $\resurrect[\evar]{-}$ are monotone.
The operation $\resurrect-$ means \emph{going to the type world (and
  shape equality)} and
the inverse operation $\resurrect[\ominus]-$ means \emph{going to the
  term world (and exact equality)}.
Further laws:
\begin{enumerate}
\item $\resurrect[\evar_3]{(\resurrect[\evar_2]{\evar_1})} =
  \resurrect[(\evar_2\evar_3)]{\evar_1}$.  
  (Proof: If $\evar_1 = \noterased$ or 
   $\erased \in \{\evar_2,\evar_3\}$ then the result is $\noterased$
   on both sides.
   Relevance level $\noterased \in \{\evar_2,\evar_3\}$ is ignored in
   composition and is neutral
   as exponent.  In the remaining case, $\evar_2 = \evar_3 =
   \nonstrict$, and we conclude by idempotency.) 
\item $\resurrect{\evar_1} \leq \evar_2$ iff $\evar_1 \leq
  \resurrect[\ominus]{\evar_2}$  (Galois connection)
  iff $\evar_1 \leq \evar_2$ 
  or $\evar_1 = \erased$ and $\evar_2 = \nonstrict$.
\item $\resurrect{(\resurrect[\ominus]{\evar})} = \resurrect\evar$
  and $\resurrect[\ominus]{(\resurrect[\oplus]\evar)} = 
  \resurrect[\ominus]\evar$.
\item $\resurrect[\evar_2]{(\resurrect\evar_1)}
       = \resurrect[{\resurrect[\ominus]{\evar_2}}]{\evar_1}$, in
       particular,
 $\nsresurrect{(\resurrect\evar)} 
  = \resurrect[{\resurrect[\ominus]{\nonstrict}}]{\evar}
  = \erresurrect\evar = {:}$.
\end{enumerate}


These operations are lifted to contexts $\Gamma$ by
applying them to the relevance operations of all bindings of $\Gamma$,
the relevant ($x \of U$), shape-irrelevant ($x \nsof U$), 
and irrelevant ($x \erof U$) ones.  

Resurrection $\resurrect\Gamma$ turns all irrelevant bindings
$x \erof T$ into shape-irrelevant $x \nsof T$ ones.
Operation $\resurrect[\noterased]\Gamma$ returns just $\Gamma$,
$\resurrect[\nonstrict]\Gamma$ makes all shape-irrelevant bindings relevant,
and $\resurrect[\erased]\Gamma$ makes \emph{all} bindings relevant.

We can extend relevance composition to include the symbols $\oplus$
and $\ominus$; let $o ::= \evar \mid \oplus \mid \ominus$.  Relevance
$\noterased$ remains the neutral element of composition, and $\erased$
the dominant element.  Altogether, we get a non-commutative operation 
with the following laws:
\begin{enumerate}
\item $\noterased\, o = o\, \noterased = o$ and $\erased\, o = o\, \erased = \erased$.
\item $\oplus \ominus = \ominus$ and $\ominus \oplus = \oplus$.
\item $\ominus \nonstrict = \ominus$ and $\nonstrict \ominus =
  \nonstrict$.
\item $\oplus \nonstrict = \erased$, 
  but $\resurrect[\nonstrict \oplus]\Gamma$ is a new
  context operation, a kind of ``decrement'', making shape-irrelevant
  assumptions relevant, and irrelevant ones shape-irrelevant.
\end{enumerate}
We extend the relevance ordering by $\erased \geq \oplus \geq
\noterased \geq \ominus$.  Note that $\oplus$ and $\nonstrict$ are
incomparable.  We have $\forall \evar(\evar^o \leq \evar^{o'})$ 
iff $o \geq o'$.  It does not make sense to extend exponentiation to
$o^{o'}$, since while the exponent may be an arbitrary context
operation, the base must be a relevance level.



\section{Declarative Presentation}


\paradot{Judgements}
\[
\begin{array}{@{}l@{\quad}l}
  \Gamma \der T  & \mbox{$T$ is a wellformed type in context $\Gamma$}
  \\
  \Gamma \der t : T & \mbox{$t$ has type $T$ in context $\Gamma$} \\
  \\
  \Gamma \der T = T' & \mbox{$T$ and $T'$ are equal types in context $\Gamma$}
  \\
  \Gamma \der t = t' : T & \mbox{$t$ and $t$' are equal terms of type $T$ in context $\Gamma$} \\
\end{array}
\]

\paradot{Derived Judgements}
\[
\begin{array}{@{}l@{\quad}l}
  \Delta \der_\Gamma p : T & \mbox{$p$ is a wellformed pattern of type
    $T$ with pattern variables $\Delta$} \\
\\
  \Gamma \der P & \mbox{$P$ is a well-formed unification problem in
    context $\Gamma$} 
  \\
  \nounify \Gamma P & \mbox{unification problem $P$ is unsolvable} \\
  \mgunify \Gamma P {\Gamma'} \sigma \tau & \mbox{unification problem
    $P$ has most general solution $\sigma,\tau$}\\
\end{array}
\]

\paradot{Pattern typing}
\[
  \Delta \der_\Gamma p : T \defas 
    \Gamma \der T             \mand 
    \Gamma\cxtsep\Delta \der p : T  \mand
    \FV(p) = \cdom\Delta
\]

\paradot{Well-formed unification problems}
\[
\ru{\Gamma \der T \qquad
    \nsresurrect\Gamma \der t : T \qquad
    \Gamma \der \Delta \qquad
    \nsresurrect\Delta \der_{\nsresurrect\Gamma} p : T
  }{\Gamma \der \unifP \Delta p t T}
\]

\paradot{Typing} 
Invariant: $\Gamma \der t : T$ implies $\resurrect\Gamma \der T$.

Basic types.
\begin{gather*}
        \ru{}{\Gamma\der 1} \qquad \ru{}{\Gamma\der ():1} \qquad
        \ru{\Gamma\der t*1}{\Gamma\der t=()*T}
        \\[1em]
        \ru{\Gamma \der A \qquad \Gamma \der B}{\Gamma \der A + B} \qquad
        \ru{\Gamma \der x:A \qquad \Gamma\der A \qquad \Gamma\der B
        }{\Gamma \der (\inl x) : (A + B)} \qquad
        \ru{\Gamma \der x:A \qquad \Gamma\der A \qquad \Gamma\der B
        }{\Gamma \der (\inr x) : (B + A)}
        \\[1em]
        \ru{\Gamma \der r : (A + B) \qquad \Gamma \der s : A\rightarrow C
        \qquad \Gamma \der t : B\rightarrow C}{
        \Gamma\der(\caseof[C] r s t) : C}
        \\[1em]
        \ru{\Gamma.x*A \der B}{\Gamma \der (x*A) \times B} \qquad
        \ru{\Gamma.x*A \der y:B}{\Gamma \der (x,y):((x*A)\times B)}
        \\[1em]
        \ru{\Gamma\der t:(x*A)\times B \qquad
                       \Gamma\der f:(z*A)\rightarrow B[x:=z] \rightarrow C}
        {\Gamma\der (\unpair[C] t f):C}
\end{gather*}

Term equality.
\begin{gather*}
        \ru{\Gamma \der t:T}{\Gamma \der t=t:T} \qquad \ru{\Gamma \der
        \subst x t p : \subst x t Q \qquad \Gamma \der t = s : T}{\Gamma\der
        \subst x s p : \subst x s Q}{\;s,t\mbox{ free for }x\mbox{ in }p,
        Q} \\[1em] \ru{\Gamma \der s=t:T}{\Gamma \der
        t=s:T} \qquad \ru{\Gamma \der t : T}{\Gamma\der s = t : T}{\;s
        =_{\beta\eta} t}
\end{gather*}

Type equality.
\begin{gather*}
 \ru{\Gamma\der T}{\Gamma\der T=T} \qquad \ru{\Gamma\der
 \subst x t T\qquad\Gamma\der t=u:V}{\Gamma\der \subst x t T  =
 \subst x u T}{\;t,u\mbox{ free for }x\mbox{ in }T} \\[1em] \ru{\Gamma\der
 x:T\qquad\Gamma\der T=U}{\Gamma\der x:U}
\end{gather*}

Functions.
\begin{gather*}
  \ru{\Gamma \der U \qquad  \eext[{\resurrect\evar}] \Gamma x U \der T
      %\Gamma\cxtsep  x \evarof U \der T
    }{\Gamma \der \efunT x U T}
\\[1em]
\mbox{instances: }\quad
  \ru{\Gamma \der U \qquad \cext \Gamma x U \der T
    }{\Gamma \der \funT x U T}
\qquad
  \ru{\Gamma \der U \qquad \nsext \Gamma x U \der T
    }{\Gamma \der \sifunT x U T}
\qquad
  \ru{\Gamma \der U \qquad \nsext \Gamma x U \der T
    }{\Gamma \der \erfunT x U T}  
\\[1em]
  \rux{(x \evarof U) \in \Gamma
     }{\Gamma \der x : U
     }{\evar = \noterased}  
\qquad
  \ru{\eext \Gamma x U \der t : T
    }{\Gamma \der \lambda x t : \efunT x U T} 
\qquad
  \ru{\Gamma \der r : \efunT x U T \qquad
      \eresurrect\Gamma \der u : U
    }{\Gamma \der r \,u : \subst u x T}
\end{gather*}

Unification constraints.
\begin{gather*}
  \ru{%\nsresurrect\Gamma \der t : T \qquad 
      %\nsresurrect\Delta \der_{\nsresurrect\Gamma} p : T \qquad
      \Gamma \der \unifP \Delta p t T \qquad
      \Gamma\cxtsep \Delta \der U
    }{\Gamma \der \unifT \Delta p t T U}
\\[0.7em]
  \ru{%\Gamma' \der \tau : \Gamma \qquad
      %\Gamma' \der \sigma : \Delta[\tau] \qquad
      %\Gamma' \der p[\sigma] = t[\tau] : T[\tau,\sigma] \qquad
      \mgunify \Gamma P {\Gamma'}\sigma\tau \qquad
      \Gamma' \der u[\tau] : U[\tau,\sigma]
    }{\Gamma  \der u : \unifA P U}
\\[0.7em]
  \ru{\Gamma \der r : \unifA P S \qquad 
      \nounify {\resurrect\Gamma} P
    }{\Gamma \der \splitno r : U}
\\[0.7em]
  \ru{\Gamma \der r : \unifA P S \qquad 
      \mgunify {\resurrect\Gamma} P {\Gamma'}\sigma\tau \qquad
      \Gamma', x \of S[\tau,\sigma] \der u[\tau,\sigma] : U[\tau]
    }{\Gamma \der \splitin r {\cdom P} x u : U}
\end{gather*}
% \begin{gather*}
%   \ru{%\nsresurrect\Gamma \der t : T \qquad 
%       %\nsresurrect\Delta \der_{\nsresurrect\Gamma} p : T \qquad
%       \Gamma \der \unifP \Delta p t T \qquad
%       \Gamma\cxtsep \Delta \der U
%     }{\Gamma \der \unifT \Delta p t T U}
% \\[0.7em]
%   \ru{%\Gamma' \der \tau : \Gamma \qquad
%       %\Gamma' \der \sigma : \Delta[\tau] \qquad
%       %\Gamma' \der p[\sigma] = t[\tau] : T[\tau,\sigma] \qquad
%       \unify \Delta {\Gamma} p t T {\Gamma'}\sigma\tau \qquad
%       \Gamma' \der u[\tau] : U[\tau,\sigma]
%     }{\Gamma  \der u : \unifT \Delta p t T U}
% \\[0.7em]
%   \ru{\Gamma \der r : \unifT \Delta p t T S \qquad 
%       \disunify \Delta {\resurrect\Gamma} p t T 
%     }{\Gamma \der \splitno r : U}
% \\[0.7em]
%   \ru{\Gamma \der r : \unifT \Delta p t T S \qquad 
%       %\Delta \der_\Gamma p : T \qquad
%       \unify \Delta {\resurrect\Gamma} p t T {\Gamma'}\sigma\tau \qquad
% %      \Gamma' \der p[\sigma] = t[\tau] : T[\tau,\sigma] \qquad
%       \Gamma', x \of S[\tau,\sigma] \der u[\tau,\sigma] : U[\tau]
%     }{\Gamma \der \splitin r {\underline\Delta} x u : U}
% \end{gather*}
Recursion.
\begin{gather*}
  \ru{\Gamma \der t : F\,(\mu F)\,\vec t
    }{\Gamma \der \tin\,t : \mu F\,\vec t}
\qquad
  \ru{\Gamma \der r : \mu F\,\vec t
    }{\Gamma \der \tout\,r : F\,(\mu F)\,\vec t}
\\[0.7em]
  \ru{\Gamma\cxtsep  \Delta\cxtsep x \of \mu F \underline\Delta \der C[\underline\Delta,x] \\
      \Gamma \der f : (\vec y : \Delta\cxtsep \, y : 
        F\,((\Delta\cxtsep x \of \mu F \underline\Delta\vec y) \times C[\underline\Delta,x])) \to
      C[\vec y,\tin\,y] 
    }{\Gamma \der \rec[\underline\Delta,x.C[\underline\Delta,x{]}]f : (\Delta\cxtsep \x \of \mu F \underline\Delta) \to C[\underline\Delta,x]}
\end{gather*}

\paradot{Relevance-relative typing}
\fbox{$\Gamma \der t \evarof T$} iff $\resurrect[\evar]\Gamma \der t : T$.

\paradot{Substitution typing} 
\fbox{$\Gamma \der \sigma : \Delta$} iff 
$\Gamma \der \sigma(x) \evarof T$ for all $(x \evarof T) \in \Delta$.

\begin{lemma}[Substitution]
  If $\Gamma \der \sigma : \Delta$ and $\Delta \der t : T$ then 
  $\Gamma \der t \sigma : T \sigma$.
\end{lemma}
\begin{lemma}[Substitution promotion] \hfill
  \begin{enumerate}
  \item $\oplus \evar_0^\oplus \geq \evar_0$ and 
    $\evar \evar_0^{\evar} \geq \evar_0$.
  \item
  If $\Gamma \der \sigma : \Delta$ then 
  $\resurrect\Gamma \der \sigma : \resurrect\Delta$ and
  $\eresurrect\Gamma \der \sigma : \eresurrect\Delta$.
  \end{enumerate}
\end{lemma}

\begin{example}[Booleans]
\[
\begin{array}{@{}lll@{\quad}l}
  \Bool   & :  & \Set \\ 
  \Bool   & := & 1 + 1 \\[0.5em]
  \tfalse, 
  \ttrue  & :  & \Bool \\
  \tfalse & := & \inl ()\\
  \ttrue  & := & \inr ()\\[1em]
\end{array}
\]
\end{example}
\begin{example}[Empty type]
\[
\begin{array}{@{}lll}
  0 & :  & \Set \\
  0 & := & \unifT \cempty \ttrue \tfalse \Bool 1 \\
  \abort[A : \Set] & : & 0 \to A \\
  \abort[A] r & := & \splitno r\\ 
\end{array}
\]
\end{example}
\begin{example}[Option type]
\[
\begin{array}{@{}lll@{\quad}l}
  \Maybe  & :  & \Set \to \Set \\
  \Maybe  & :  & \lambda A.\, 1 + A \\[0.5em]
  \nothing[A : \Set] & : & \Maybe\, A \\
  \nothing[A] & := & \inl () \\[0.5em]
  \just[A : \Set] & : & A \to \Maybe A \\
  \just[A] x & := & \inr x \\[0.5em]
  \maybe[A : \Set, C[x : \Maybe A{]}] & : & 
    C[\nothing] \to ((y \of A) \to C[\just y]) \to % \\ && 
    (x \of \Maybe A) \to C[x] \\
  \maybe[A,C[x{]}] & := & \lam n \lam j \lam x \caseof x {\lamu n} j \\[1em]
\end{array}
\]
\end{example}

\begin{example}[Natural numbers]
\[
\begin{array}{@{}lll@{\qquad}l}
  % \_+\_    & : & \Set \to \Set \to \Set \\ 
  % T_1 + T_2 & := & \sigT x 2 {\ifte x {T_1}{T_2}} 
  %  & \mbox{disjoint sum} \\[0.5em]
  % \tinl    & : &
  \Nat    & :  & \Set \\
  \Nat    & := & \mu\, \Maybe \\[0.5em]
  \tzero  & :  & \Nat \\
  \tzero  & := & \tin\,\nothing \\[0.5em]
  % \tzero  & := & \inp{\inl ()} \\
  \tsuc   & :  & \Nat \to \Nat \\
  \suc x  & := & \inp{\just x} \\
\end{array}
\]  
Specialized recursor for natural numbers:
% \[
%   \ru{\Gamma\cxtsep  x \of \Nat \der C[x] \qquad \Gamma \der z : C[\tzero] \\
%       \Gamma \der s : (x \of \Nat) \to C[x] \to C[\suc x]
%     }{\Gamma \der \natrec C z s : (x \of Nat) \to C [x]}
% \]
\[
\begin{array}{@{}lll@{\quad}l}
  \natrec[C[x : \Nat{]}] & : & C[\tzero] 
              \to ((x \of \Nat) \to C[x] \to C[\suc x]) 
              \to (x \of \Nat) \to C[x] \\
%   & \mwhere x \of \Nat \der C \\
  \natrec[C] & := & \lam z \lam s \rec[C] \dots \\
\end{array}
\]
\end{example}
\begin{example}[Recursive vectors]
\[
  \begin{array}{@{}llll}
\RVec & :  & \Set \to \Nat \to \Set \\
\RVec & := & \lam A \natrec[\_.\Set] 1 {(\lam \_ \lam X  A \times X)} \\[0.5em]
\rnil[A : \Set]  & :  & \RVec\,A\,\tzero \\
\rnil[A]         & := & () \\[0.5em]
\rcons[A : \Set] & :  & (n \of \Nat) \to A \to \RVec\,A\,n \to \RVec\,A\,(\suc n)\\  
\rcons[A]\,n\,x\,\vxs & := & (x,\vxs) \\
  \end{array}
\]
\end{example}
\begin{example}[Inductive vectors, equality encoding]
\[
  \begin{array}{@{}llll}
\IVec & :  & \Set \to \Nat \sito \Set \\
\IVec & := & \lam A \mu\, \lam {X : \Nat \sito \Set} \lam {n \nsof \Nat}
  (\Eq n \tzero) + \sisigT m \Nat (\Eq n {\suc m}) \times A \times X\,m \\[0.5em]
\inil[A : \Set]  & :  & \IVec\,A\;\tzero \\
\inil[A]         & := & \inp {\inl \trefl} \\[0.5em]
\icons[A : \Set] & :  & \sifunT n \Nat  A \to \IVec\,A\,n \to \IVec\,A\,(\suc n)\\  
\icons[A]\,n\,x\,\vxs & := & \tin\,(\inr{(m,(\trefl,(x,\vxs))))} \\
  \end{array}
\]
\end{example}
\begin{example}[Inductive vectors, constraint encoding]
\[
  \begin{array}{@{}llll}
\IVec & :  & \Set \to \Nat \sito \Set \\
\IVec & := & \lam A \mu\, \lam {X : \Nat \sito \Set} \lam {n \nsof \Nat} 
\\ &&
  (\unifT \cempty \tzero n \Nat 1) + 
  (\unifT {m\nsof\Nat} {\suc m} n \Nat {A \times X\,m}) \\[0.5em]
\inil[A : \Set]  & :  & \IVec\,A\;\tzero \\
\inil[A]         & := & \inp {\inl ()} \\[0.5em]
\icons[A : \Set] & :  & \erfunT n \Nat  A \to \IVec\,A\,n \to \IVec\,A\,(\suc n)\\  
\icons[A]\,n\,x\,\vxs & := & \tin\,(\inr {(x,\vxs)}) \\
  \end{array}
\]
Excerpts of typing derivations: Case $\IVec$.  
Let $\Gamma = \nsext{\cext{A : \Set} X {\Nat \sito \Set}} n \Nat$.
\[
\begin{prooftree}
    \[
      m : \Nat \der_{\nsresurrect{\Gamma}} \suc m : \Nat
      \qquad
      \nsresurrect{\Gamma} \der n : \Nat
    \justifies
    \Gamma \der \unifP {m\nsof\Nat} {\suc m} n \Nat
    \] 
  \qquad
    \[
      \[
      \cext{\nsresurrect \Gamma} m \Nat \der m : \Nat
      \justifies
      \nsext \Gamma m \Nat \der X\,m
      \]
    \justifies
    \nsext \Gamma m \Nat \der A \times X\,m
    \]
  \justifies
  \Gamma \der \unifT {m\nsof\Nat} {\suc m} n \Nat {A \times X\,m}
\end{prooftree}
\]
Case $\icons$.  Let $\Gamma = \cext{\cext{\erext{A \of \Set} n \Nat} x
  A} \vxs {\IVec\,A\,n}$.
\[
\begin{prooftree}
  \[
    \unify {m \nsof \Nat} {\Gamma} {m} {n} \Nat \Gamma
  \sid {[n/m]}
    \justifies
    \unify {m \nsof \Nat} {\Gamma} {\suc m} {\suc n} \Nat \Gamma
  \sid {[n/m]}
  \] 
  \qquad  
  \[\Gamma \der \vxs : \IVec\, A\, n
    \justifies
    \Gamma \der (x,\vxs) : A \times \IVec\,A\,n
  \]
  \justifies
  \Gamma \der (x,\vxs) : (\unifT {m\nsof\Nat} {\suc m} {\suc n} \Nat {A \times \IVec\,A\,m})
\end{prooftree}
\]
\end{example}





\section{Algorithmic Presentation}


\paradot{Judgements}
\[
\begin{array}{@{}l@{\quad}l}
  \Gamma \dera T  & \mbox{$T$ is a wellformed type in context $\Gamma$}
  \\
  \Gamma \dera t \jchk T & \mbox{$t$ checks against type $T$ in context $\Gamma$} \\
  \Gamma \dera r \jinf T & \mbox{$r$ has inferred type $T$ in context $\Gamma$} \\
  \\
  \Gamma \dera P & \mbox{$P$ is a well-formed unification problem in
    context $\Gamma$} 
  \\
  \disunify \Delta \Gamma p t T & 
    \mbox{unification of expression $t$ and pattern $p$ fails} \\
  \unify \Delta \Gamma p t T {\Gamma'} \sigma \tau & 
    \mbox{expression $t$ unifies with pattern
    $p$ under m.g.u. $\sigma,\tau$}\\
\end{array}
\]


\paradot{Unification}

\fbox{$\unify \Delta \Gamma p t T {\Gamma'} \tau \sigma$}\\[0.5em]

\paradot{Algorithm for unification}

Concatenation of pairs of substitutions are meant component-wise,
concatenation with $\contradict$ yields $\contradict$. $z$ is always a
new variable which has not been used yet, $q$ and $r$ are placeholders
for either $(\cdot,\cdot)$, or for $\tin$ $\inl$ $\inr$ ignoring the
second argument.

\begin{eqnarray*}
        \unifFun x y &=& ({\subst x {z} {}},{\subst y {z}
        {}}) \\ \unifFun x {q(t,u)} &=& ({\subst x {\subst x z
        {q(t,u)}} {}}, \subst x z {}) \\ \unifFun {q(t,u)} x
        &=& \left\{ \begin{array}{cl}(\tau,\sigma) & \mbox{for
        }\unifFun x {q(t,u)} = (\sigma,\tau)\\ \contradict & \mbox{for
        }\unifFun x {q(t,u)}
        = \contradict \end{array}\right.\\ \unifFun {q(t,u)} {r(v,w)}
        &=& \left\{\begin{array}{cl} (\unifFun t v) \circ (\unifFun u
        w) & \mbox{for } q = r \\ \contradict
        & \mbox{otherwise}\end{array}\right.
\end{eqnarray*}

Invariants:
If $\resurrect \Gamma \der T$ and
$\resurrect \Gamma \der \Delta$ and
$\nsresurrect{\resurrect{\Gamma}} \der t : T$ and
$\nsresurrect{\Delta} \der_{\nsresurrect{{\resurrect \Gamma}}} p : T$ then
$\Gamma' \der \tau : \Gamma$ and
$\resurrect{\Gamma'} \der \sigma : \Delta\tau$ and
$\nsresurrect{{\resurrect{{\Gamma'}}}} \der p\sigma = t \tau : T \tau$.
Remember that $\nsresurrect{{\resurrect\Gamma}} = \erresurrect{\Gamma}$.
\begin{gather*}
  \ru{
    }{\unify \Delta \Gamma x t T \Gamma \sid {\sg t x}}
\qquad
  \ru{
    }{\unify \Delta {\Gamma\cxtsep  y \evarof T, \Gamma'} p y T
      {\Gamma\cxtsep \Delta\cxtsep\Gamma'} {\sg p y} \sid} 
\end{gather*}



\bibliographystyle{alpha}
\bibliography{auto-shapeIrr}

\end{document}
