...

[bitonic-mengthesis.git] / thesis.lagda

\documentclass[report]{article}

%% Narrow margins
% \usepackage{fullpage}

%% Bibtex
\usepackage{natbib}

%% Links
\usepackage{hyperref}

%% Frames
\usepackage{framed}

%% Symbols
\usepackage[fleqn]{amsmath}
\usepackage{stmaryrd}           %llbracket

%% Proof trees
\usepackage{bussproofs}

%% Diagrams
\usepackage[all]{xy}

%% Quotations
\usepackage{epigraph}

%% Images
\usepackage{graphicx}

%% diagrams
\usepackage{tikz}
\usetikzlibrary{shapes,arrows,positioning}
% \usepackage{tikz-cd}
% \usepackage{pgfplots}


%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\usepackage[conor]{agda}
\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\renewcommand{\AgdaField}{\AgdaFunction}
% \definecolor{AgdaBound} {HTML}{000000}
\definecolor{AgdaHole} {HTML} {FFFF33}

\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
\DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
\DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
\DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
\DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}


%% -----------------------------------------------------------------------------
%% Commands

\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
% TODO make this use AgdaBound
\newcommand{\myb}[1]{\AgdaBound{#1}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textsc{Kant}}
\newcommand{\mysynel}[1]{#1}
\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\mysp}{\ }
% TODO \mathbin or \mathre here?
\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
\newcommand{\myappsp}{\hspace{0.07cm}}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\newcommand{\mysynsep}{\ \ |\ \ }

\FrameSep0.2cm
\newcommand{\mydesc}[3]{
  \noindent
  \mbox{
    \parbox{\textwidth}{
      {\small
        \vspace{0.3cm}
        \hfill \textbf{#1} $#2$

        \framebox[\textwidth]{
          \parbox{\textwidth}{
            \vspace{0.1cm}
            #3
            \vspace{0.1cm}
          }
        }
      }
    }
  }
}

% TODO is \mathbin the correct thing for arrow and times?

\newcommand{\mytmt}{\mysynel{t}}
\newcommand{\mytmm}{\mysynel{m}}
\newcommand{\mytmn}{\mysynel{n}}
\newcommand{\myred}{\leadsto}
\newcommand{\mysub}[3]{#1[#2 / #3]}
\newcommand{\mytysyn}{\mysynel{type}}
\newcommand{\mybasetys}{K}
% TODO change this name
\newcommand{\mybasety}[1]{B_{#1}}
\newcommand{\mytya}{\myse{A}}
\newcommand{\mytyb}{\myse{B}}
\newcommand{\mytycc}{\myse{C}}
\newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
\newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
\newcommand{\myctx}{\Gamma}
\newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
\newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
\newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
% TODO \mathbin or \mathrel here?
\newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
\newcommand{\mytt}{\mydc{$\langle\rangle$}}
\newcommand{\myunit}{\mytyc{Unit}}
\newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
\newcommand{\myfst}{\myfld{fst}}
\newcommand{\mysnd}{\myfld{snd}}
\newcommand{\myconst}{\myse{c}}
\newcommand{\myemptyctx}{\cdot}
\newcommand{\myhole}{\AgdaHole}
\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
\newcommand{\myleft}[1]{\mydc{left}_{#1}}
\newcommand{\myright}[1]{\mydc{right}_{#1}}
\newcommand{\myempty}{\mytyc{Empty}}
\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
\newcommand{\myarg}{\_}
\newcommand{\myderivsp}{\vspace{0.3cm}}
\newcommand{\mytyp}{\mytyc{Type}}
\newcommand{\myneg}{\myfun{$\neg$}}
\newcommand{\myar}{\,}
\newcommand{\mybool}{\mytyc{Bool}}
\newcommand{\mytrue}{\mydc{true}}
\newcommand{\myfalse}{\mydc{false}}
\newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
\newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
\newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
\newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
\newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
\newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
\newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
\newcommand{\mylist}{\mytyc{List}}
\newcommand{\mynil}[1]{\mydc{[]}_{#1}}
\newcommand{\mycons}{\mathbin{\mydc{∷}}}
\newcommand{\myfoldr}{\myfun{foldr}}
\newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
\newcommand{\mynode}[2]{\mathbin{\mydc{$\lhd$}_{#1.#2}}}
\newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
\newcommand{\mylub}{\sqcup}
\newcommand{\mydefeq}{\cong}
\newcommand{\myrefl}{\mydc{refl}}
\newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
\newcommand{\myjeqq}{\myfun{=-elim}}
\newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
\newcommand{\mysubst}{\myfun{subst}}
\newcommand{\myprsyn}{\myse{prop}}
\newcommand{\myprdec}[1]{\llbracket #1 \rrbracket}
\newcommand{\myand}{\wedge}
\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
\newcommand{\mybot}{\bot}
\newcommand{\mytop}{\top}
\newcommand{\mycoe}{\myfun{coe}}
\newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
\newcommand{\mycoh}{\myfun{coh}}
\newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
\newcommand{\myjm}[4]{(#1 {:} #2) = (#3 {:} #4)}
\newcommand{\myprop}{\mytyc{Prop}}

%% -----------------------------------------------------------------------------

\title{\mykant: Implementing Observational Equality}
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{June 2013}

\begin{document}

\iffalse
\begin{code}
module thesis where
\end{code}
\fi

\maketitle

\begin{abstract}
  The marriage between programming and logic has been a very fertile one.  In
  particular, since the simply typed lambda calculus (STLC), a number of type
  systems have been devised with increasing expressive power.

  Section \ref{sec:types} will give a very brief overview of STLC, and then
  illustrate how it can be interpreted as a natural deduction system.  Section
  \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
  on this concept, employing a more expressive logic.  The exposition is quite
  dense since there is a lot of material to cover; for a more complete treatment
  of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
  Section \ref{sec:equality} will explain why equality has always been a tricky
  business in these theories, and talk about the various attempts that have been
  made to make the situation better.  One interesting development has recently
  emerged: Observational Type theory.

  Section \ref{sec:practical} will describe common extensions found in the
  systems currently in use.  Finally, section \ref{sec:kant} will describe a
  system developed by the author that implements a core calculus based on the
  principles described.
\end{abstract}

\clearpage

\tableofcontents

\clearpage

\section{Simple and not-so-simple types}
\label{sec:types}

\subsection{The untyped $\lambda$-calculus}

Along with Turing's machines, the earliest attempts to formalise computation
lead to the $\lambda$-calculus \citep{Church1936}.  This early programming
language encodes computation with a minimal syntax and no `data' in the
traditional sense, but just functions.  Here we give a brief overview of the
language, which will give the chance to introduce concepts central to the
analysis of all the following calculi.  The exposition follows the one found in
chapter 5 of \cite{Queinnec2003}.

The syntax of $\lambda$-terms consists of three things: variables, abstractions,
and applications:

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
    x          & \in & \text{Some enumerable set of symbols}
  \end{array}
  $
}

Parenthesis will be omitted in the usual way:
$\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
\myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.

Abstractions roughly corresponds to functions, and their semantics is more
formally explained by the $\beta$-reduction rule:

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  $
  \begin{array}{l}
    \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
    \myind{1}
    \begin{array}{l@{\ }c@{\ }l}
      \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
      \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
      \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
      \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
      \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
      \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
    \end{array}
  \end{array}
  $
}

The care required during substituting variables for terms is required to avoid
name capturing.  We will use substitution in the future for other name-binding
constructs assuming similar precautions.

These few elements are of remarkable expressiveness, and in fact Turing
complete.  As a corollary, we must be able to devise a term that reduces forever
(`loops' in imperative terms):
\[
  (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
\]

A \emph{redex} is a term that can be reduced.  In the untyped $\lambda$-calculus
this will be the case for an application in which the first term is an
abstraction, but in general we call aterm reducible if it appears to the left of
a reduction rule.  When a term contains no redexes it's said to be in
\emph{normal form}.  Given the observation above, not all terms reduce to a
normal forms: we call the ones that do \emph{normalising}, and the ones that
don't \emph{non-normalising}.

The reduction rule presented is not syntax directed, but \emph{evaluation
  strategies} can be employed to reduce term systematically. Common evaluation
strategies include \emph{call by value} (or \emph{strict}), where arguments of
abstractions are reduced before being applied to the abstraction; and conversely
\emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
to proceed---in other words when we have an application where the function is
still not a $\lambda$. In both these reduction strategies we never reduce under
an abstraction: for this reason a weaker form of normalisation is used, where
both abstractions and normal forms are said to be in \emph{weak head normal
  form}.

\subsection{The simply typed $\lambda$-calculus}

A convenient way to `discipline' and reason about $\lambda$-terms is to assign
\emph{types} to them, and then check that the terms that we are forming make
sense given our typing rules \citep{Curry1934}.  The first most basic instance
of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
rules are shown in figure \ref{fig:stlc}.

Our types contain a set of \emph{type variables} $\Phi$, which might correspond
to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
types of functions.  The language is explicitly typed: when we bring a variable
into scope with an abstraction, we explicitly declare its type. $\mytya$,
$\mytyb$, $\mytycc$, will be used to refer to a generic type.  Reduction is
unchanged from the untyped $\lambda$-calculus.

\begin{figure}[t]
  \mydesc{syntax}{ }{
    $
    \begin{array}{r@{\ }c@{\ }l}
      \mytmsyn   & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
      (\myapp{\mytmsyn}{\mytmsyn}) \\
      \mytysyn   & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn  \mysynsep \\
      \myb{x}    & \in & \text{Some enumerable set of symbols} \\
      \myse{\phi} & \in & \Phi
    \end{array}
    $
  }
  
  \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
    \centering{
      \begin{tabular}{ccc}
        \AxiomC{$\myctx(x) = A$}
        \UnaryInfC{$\myjud{\myb{x}}{A}$}
        \DisplayProof
        &
        \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
        \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
        \DisplayProof
        &
        \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
        \AxiomC{$\myjud{\mytmn}{\mytya}$}
        \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
        \DisplayProof
      \end{tabular}
    }
}
  \caption{Syntax and typing rules for the STLC.  Reduction is unchanged from
    the untyped $\lambda$-calculus.}
  \label{fig:stlc}
\end{figure}

In the typing rules, a context $\myctx$ is used to store the types of bound
variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
$\myctx(x)$ returns the type of the rightmost occurrence of $x$.

This typing system takes the name of `simply typed lambda calculus' (STLC), and
enjoys a number of properties.  Two of them are expected in most type systems
\citep{Pierce2002}:
\begin{description}
\item[Progress] A well-typed term is not stuck---it is either a variable, or its
  constructor does not appear on the left of the $\myred$ relation (currently
  only $\lambda$), or it can take a step according to the evaluation rules.
\item[Preservation] If a well-typed term takes a step of evaluation, then the
  resulting term is also well-typed, and preserves the previous type.  Also
  known as \emph{subject reduction}.
\end{description}

However, STLC buys us much more: every well-typed term is normalising
\citep{Tait1967}.  It is easy to see that we can't fill the blanks if we want to
give types to the non-normalising term shown before:
\begin{equation*}
  \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
\end{equation*}

This makes the STLC Turing incomplete.  We can recover the ability to loop by
adding a combinator that recurses:

\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ } {
  $ \mytmsyn ::= \dotsb \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
  \vspace{0.4cm}
}
\end{minipage} 
\begin{minipage}{0.5\textwidth}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
  \centering{
    \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
    \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
    \DisplayProof
  }
}
\end{minipage} 

\mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \centering{
    $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
  }
}

This will deprive us of normalisation, which is a particularly bad thing if we
want to use the STLC as described in the next section.

\subsection{The Curry-Howard correspondence}

It turns out that the STLC can be seen a natural deduction system for
intuitionistic propositional logic.  Terms are proofs, and their types are the
propositions they prove.  This remarkable fact is known as the Curry-Howard
correspondence, or isomorphism.

The arrow ($\myarr$) type corresponds to implication.  If we wish to prove that
that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
\myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
correct type:
\[
  \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
\]
That is, function composition.  Going beyond arrow types, we can extend our bare
lambda calculus with useful types to represent other logical constructs, as
shown in figure \ref{fig:natded}.

\begin{figure}[t]
\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \dots \\
             &  |  & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
             &  |  & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
                     \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
                     \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
             &  |  & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
                     \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
    \mytysyn & ::= & \dots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
  \end{array}
  $
}

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  \centering{
    \begin{tabular}{cc}
      $
      \begin{array}{l@{ }l@{\ }c@{\ }l}
        \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
          \myapp{\mytmm}{\mytmt} \\
        \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
          \myapp{\mytmn}{\mytmt}
      \end{array}
      $
      &
      $
      \begin{array}{l@{ }l@{\ }c@{\ }l}
        \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
        \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
      \end{array}
      $
    \end{tabular}
  }
}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  \centering{
    \begin{tabular}{cc}
      \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
      \UnaryInfC{$\myjud{\mytt}{\myunit}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\myempty}$}
      \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
      \DisplayProof
    \end{tabular}
  }
  \myderivsp
  \centering{
    \begin{tabular}{cc}
      \AxiomC{$\myjud{\mytmt}{\mytya}$}
      \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\mytyb}$}
      \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
      \DisplayProof

    \end{tabular}
  }
  \myderivsp
  \centering{
    \begin{tabular}{cc}
      \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
      \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
      \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
      \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
      \DisplayProof
    \end{tabular}
  }
  \myderivsp
  \centering{
    \begin{tabular}{ccc}
      \AxiomC{$\myjud{\mytmm}{\mytya}$}
      \AxiomC{$\myjud{\mytmn}{\mytyb}$}
      \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
      \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
      \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
      \DisplayProof
    \end{tabular}
  }
}
\caption{Rules for the extendend STLC.  Only the new features are shown, all the
  rules and syntax for the STLC apply here too.}
  \label{fig:natded}
\end{figure}

Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in
Haskell) correspond to disjunctions, and dually tuples (or pairs, or
products---$\myprod$ here, tuples in Haskell) correspond to conjunctions.  This
is apparent looking at the ways to construct and destruct the values inhabiting
those types: for $\mysum$ $\myleft{ }$ and $\myright{ }$ correspond to $\vee$
introduction, and $\mycase{\_}{\_}$ to $\vee$ elimination; for $\myprod$
$\mypair{\_}{\_}$ corresponds to $\wedge$ introduction, $\myfst$ and $\mysnd$ to
$\wedge$ elimination.

The trivial type $\myunit$ corresponds to the logical $\top$, and dually
$\myempty$ corresponds to the logical $\bot$.  $\myunit$ has one introduction
rule ($\mytt$), and thus one inhabitant; and no eliminators.  $\myempty$ has no
introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
}$), corresponding to the logical \emph{ex falso quodlibet}.  Note that in the
constructors for the sums and the destructor for $\myempty$ we need to include
some type information to keep type checking decidable.

With these rules, our STLC now looks remarkably similar in power and use to the
natural deduction we already know.  $\myneg \mytya$ can be expressed as $\mytya
\myarr \myempty$.  However, there is an important omission: there is no term of
the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
$\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
a type equivalent to those.

This has a considerable effect on our logic and it's no coincidence, since there
is no obvious computational behaviour for laws like the excluded middle.
Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
and all the systems analysed will have this characteristic since they build on
the foundation of the STLC\footnote{There is research to give computational
  behaviour to classical logic, but I will not touch those subjects.}.

As in logic, if we want to keep our system consistent, we must make sure that no
closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
The variant of STLC presented here is indeed
consistent, a result that follows from the fact that it is
normalising. % TODO explain
Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
desire for consistency.  The following term works for every type $\mytya$,
including bottom:
\[
(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
\]

\subsection{Inductive data}

To make the STLC more useful as a programming language or reasoning tool it is
common to include (or let the user define) inductive data types.  These comprise
of a type former, various constructors, and an eliminator (or destructor) that
serves as primitive recursor.

For example, we might add a $\mylist$ type constructor, along with an `empty
list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor.  The eliminator for
lists will be the usual folding operation ($\myfoldr$).  See figure
\ref{fig:list}.

\begin{figure}[h]
\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \dots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
                     \mysynsep
                     \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
    \mytysyn & ::= & \dots \mysynsep \myapp{\mylist}{\mytysyn}
  \end{array}
  $
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  \centering{
  $
  \begin{array}{l@{\ }c@{\ }l}
    \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\

    \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
    \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
  \end{array}
  $
}
}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  \centering{
    \begin{tabular}{cc}
      \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
      \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmm}{\mytya}$}
      \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
      \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
      \DisplayProof
    \end{tabular}
  }
  \myderivsp
  \centering{
    \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
    \AxiomC{$\myjud{\mytmm}{\mytyb}$}
    \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
    \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
    \DisplayProof
  }
}
\caption{Rules for lists in the STLC.}
\label{fig:list}
\end{figure}

In section \ref{sec:well-order} we will see how to give a general account of
inductive data.  %TODO does this make sense to have here?

\section{Intuitionistic Type Theory}
\label{sec:itt}

\subsection{Extending the STLC}

The STLC can be made more expressive in various ways.  \cite{Barendregt1991}
succinctly expressed geometrically how we can add expressivity:

$$
\xymatrix@!0@=1.5cm{
  & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
  & & \lambda C \ar@{-}[dd]
  \\
  \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
  & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
  \\
  & \lambda\underline\omega \ar@{-}'[r][rr]
  & & \lambda P\underline\omega
  \\
  \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
  & & \lambda P \ar@{-}[ur]
}
$$
Here $\lambda{\to}$, in the bottom left, is the STLC.  From there can move along
3 dimensions:
\begin{description}
\item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
  types in our type signatures.  For example, we can define a polymorphic
  identity function:
  \[\displaystyle
  (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
  \]
  The first and most famous instance of this idea has been System F.  This form
  of polymorphism and has been wildly successful, also thanks to a well known
  inference algorithm for a restricted version of System F known as
  Hindley-Milner.  Languages like Haskell and SML are based on this discipline.
\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
  type operators.  For example we could define a function that given types $R$
  and $\mytya$ forms the type that represents a value of type $\mytya$ in
  continuation passing style: \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
    \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp\]
\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
  types', give great expressive power.  For example, we can have values of whose
  type depend on a boolean:
  \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
  \myarr \mytyp\]
\end{description}

All the systems preserve the properties that make the STLC well behaved.  The
system we are going to focus on, Intuitionistic Type Theory, has all of the
above additions, and thus would sit where $\lambda{C}$ sits in the
`$\lambda$-cube'.  It will serve as the logical `core' of all the other
extensions that we will present and ultimately our implementation of a similar
logic.

\subsection{A Bit of History}

Logic frameworks and programming languages based on type theory have a long
history.  Per Martin-L\"{o}f described the first version of his theory in 1971,
but then revised it since the original version was inconsistent due to its
impredicativity\footnote{In the early version there was only one universe
  $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
  explanation on why this causes problems.}.  For this reason he gave a revised
and consistent definition later \citep{Martin-Lof1984}.

A related development is the polymorphic $\lambda$-calculus, and specifically
the previously mentioned System F, which was developed independently by Girard
and Reynolds.  An overview can be found in \citep{Reynolds1994}.  The surprising
fact is that while System F is impredicative it is still consistent and strongly
normalising.  \cite{Coquand1986} further extended this line of work with the
Calculus of Constructions (CoC).

Most widely used interactive theorem provers are based on ITT.  Popular ones
include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
\citep{McBride2004, EpigramTut}.

\subsection{A note on inference}

% TODO do this, adding links to the sections about bidi type checking and
% implicit universes.
In the following text I will often omit explicit typing for abstractions or

Moreover, I will use $\mytyp$ without bothering to specify a
universe, with the silent assumption that the definition is consistent
regarding to the hierarchy.

\subsection{A simple type theory}
\label{sec:core-tt}

The calculus I present follows the exposition in \citep{Thompson1991}, and is
quite close to the original formulation of predicative ITT as found in
\citep{Martin-Lof1984}.  The system's syntax and reduction rules are presented
in their entirety in figure \ref{fig:core-tt-syn}.  The typing rules are
presented piece by piece.  An Agda rendition of the presented theory is
reproduced in appendix \ref{app:agda-code}.

\begin{figure}[t]
\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \myb{x} \mysynsep
                     \mytyp_{l} \mysynsep
                     \myunit \mysynsep \mytt \mysynsep
                     \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
             &  |  & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
                     \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
             &  |  & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
                     \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \\
             &  |  & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
                     \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
             &  |  & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
             &  |  & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
                     \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
             &  |  & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
    l        & \in & \mathbb{N}
  \end{array}
  $
}

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  \centering{
    \begin{tabular}{cc}
      $
      \begin{array}{l@{ }l@{\ }c@{\ }l}
        \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
        \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
      \end{array}
      $
      &
      $
      \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
      $
      \myderivsp
    \end{tabular}
    $
    \begin{array}{l@{ }l@{\ }c@{\ }l}
      \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
      \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
    \end{array}
    $
    \myderivsp

    $
    \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
    \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
      \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
    })}
    $
  }
}
\caption{Syntax and reduction rules for our type theory.}
\label{fig:core-tt-syn}
\end{figure}

\subsubsection{Types are terms, some terms are types}
\label{sec:term-types}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \centering{
    \begin{tabular}{cc}
      \AxiomC{$\myjud{\mytmt}{\mytya}$}
      \AxiomC{$\mytya \mydefeq \mytyb$}
      \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
      \DisplayProof
      &
      \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
      \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
      \DisplayProof
    \end{tabular}
  }
}

The first thing to notice is that a barrier between values and types that we had
in the STLC is gone: values can appear in types, and the two are treated
uniformly in the syntax.

While the usefulness of doing this will become clear soon, a consequence is
that since types can be the result of computation, deciding type equality is
not immediate as in the STLC.  For this reason we define \emph{definitional
  equality}, $\mydefeq$, as the congruence relation extending
$\myred$---moreover, when comparing types syntactically we do it up to
renaming of bound names ($\alpha$-renaming).  For example under this
discipline we will find that
\[
\myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
\]
Types that are definitionally equal can be used interchangeably.  Here the
`conversion' rule is not syntax directed, however we will see how it is
possible to employ $\myred$ to decide term equality in a systematic
way.  % TODO add section
Another thing to notice is that considering the need to reduce terms to decide
equality, it is essential for a dependently type system to be terminating and
confluent for type checking to be decidable.

Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
$\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
$\mylist$, etc.  $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \dots$.  Each type
`level' is often called a universe in the literature.  While it is possible,
to simplify things by having only one universe $\mytyp$ with $\mytyp :
\mytyp$, this plan is inconsistent for much the same reason that impredicative
na\"{\i}ve set theory is \citep{Hurkens1995}.  Moreover, various techniques
can be employed to lift the burden of explicitly handling universes.
% TODO add sectioon about universes

\subsubsection{Contexts}

\begin{minipage}{0.5\textwidth}
  \mydesc{context validity:}{\myvalid{\myctx}}{
    \centering{
      \begin{tabular}{cc}
        \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
        \UnaryInfC{$\myvalid{\myemptyctx}$}
        \DisplayProof
        &
        \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
        \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
        \DisplayProof
      \end{tabular}
    }
  }
\end{minipage} 
\begin{minipage}{0.5\textwidth}
  \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
    \centering{
      \AxiomC{$\myctx(x) = \mytya$}
      \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
      \DisplayProof
    }
  }
\end{minipage}
\vspace{0.1cm}

We need to refine the notion context to make sure that every variable appearing
is typed correctly, or that in other words each type appearing in the context is
indeed a type and not a value.  In every other rule, if no premises are present,
we assume the context in the conclusion to be valid.

Then we can re-introduce the old rule to get the type of a variable for a
context.

\subsubsection{$\myunit$, $\myempty$}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \centering{
    \begin{tabular}{ccc}
      \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
      \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
      \noLine
      \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
      \DisplayProof
      &
      \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
      \UnaryInfC{$\myjud{\mytt}{\myunit}$}
      \noLine
      \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\myempty}$}
      \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
      \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
      \noLine
      \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
      \DisplayProof
    \end{tabular}
  }
}

Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
sure that we are invoking $\myabsurd{}$ over a type.

\subsubsection{$\mybool$, and dependent $\myfun{if}$}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
 \centering{
   \begin{tabular}{ccc}
     \AxiomC{}
     \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
     \DisplayProof
     &
     \AxiomC{}
     \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
     \DisplayProof
     &
     \AxiomC{}
      \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
      \DisplayProof
    \end{tabular}
    \myderivsp

    \AxiomC{$\myjud{\mytmt}{\mybool}$}
    \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
    \noLine
    \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
    \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
    \DisplayProof

  }
}

With booleans we get the first taste of `dependent' in `dependent types'.  While
the two introduction rules ($\mytrue$ and $\myfalse$) are not surprising, the
typing rules for $\myfun{if}$ are.  In most strongly typed languages we expect
the branches of an $\myfun{if}$ statements to be of the same type, to preserve
subject reduction, since execution could take both paths.  This is a pity, since
the type system does not reflect the fact that in each branch we gain knowledge
on the term we are branching on.  Which means that programs along the lines of
\begin{verbatim}
if null xs then head xs else 0
\end{verbatim}
are a necessary, well typed, danger.

However, in a more expressive system, we can do better: the branches' type can
depend on the value of the scrutinised boolean.  This is what the typing rule
expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
representing the scrutinised boolean type, and the branches are typechecked with
the updated knowledge on the value of $\myb{x}$.

\subsubsection{$\myarr$, or dependent function}

 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
   \centering{
     \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
     \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
     \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
     \DisplayProof

     \myderivsp

    \begin{tabular}{cc}
      \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
      \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
      \AxiomC{$\myjud{\mytmn}{\mytya}$}
      \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
      \DisplayProof
    \end{tabular}
  }
}

Dependent functions are one of the two key features that perhaps most
characterise dependent types---the other being dependent products.  With
dependent functions, the result type can depend on the value of the argument.
This feature, together with the fact that the result type might be a type
itself, brings a lot of interesting possibilities.  Keeping the correspondence
with logic alive, dependent functions are much like universal quantifiers
($\forall$) in logic.

Again, we need to make sure that the type hierarchy is respected, which is the
reason why a type formed by $\myarr$ will live in the least upper bound of the
levels of argument and return type.  This trend will continue with the other
type-level binders, $\myprod$ and $\mytyc{W}$.

% TODO maybe examples?

\subsubsection{$\myprod$, or dependent product}


\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \centering{
     \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
     \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
     \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
     \DisplayProof

     \myderivsp

    \begin{tabular}{cc}
      \AxiomC{$\myjud{\mytmm}{\mytya}$}
      \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
      \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
      \noLine
      \UnaryInfC{\phantom{$--$}}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
      \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
      \noLine
      \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
      \DisplayProof
    \end{tabular}

  }
}


\subsubsection{$\mytyc{W}$, or well-order}
\label{sec:well-order}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \centering{
     \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
     \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
     \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
     \DisplayProof

     \myderivsp

     \AxiomC{$\myjud{\mytmt}{\mytya}$}
     \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
     \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
     \DisplayProof

     \myderivsp

     \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
     \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
     \noLine
     \BinaryInfC{$\myjud{\myse{p}}{
       \myfora{\myb{s}}{\myse{S}}{\myfora{\myb{f}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}} \myarr \myw{\myb{x}}{\myse{S}}{\myse{T}}}{(\myfora{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myb{s}}}{\mysub{\myse{P}}{\myb{w}}{\myapp{\myb{f}}{\myb{t}}}}) \myarr \mysub{\myse{P}}{\myb{w}}{\myb{f}}}}
     }$}
     \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
     \DisplayProof
   }
}

\section{The struggle for equality}
\label{sec:equality}

In the previous section we saw how a type checker (or a human) needs a notion of
\emph{definitional equality}.  Beyond this meta-theoretic notion, in this
section we will explore the ways of expressing equality \emph{inside} the
theory, as a reasoning tool available to the user.  This area is the main
concern of this thesis, and in general a very active research topic, since we do
not have a fully satisfactory solution, yet.

\subsection{Propositional equality}

\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \dots \\
             &  |  & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
                     \myapp{\myrefl}{\mytmsyn} \\
             &  |  & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
  \end{array}
  $
}
\end{minipage} 
\begin{minipage}{0.5\textwidth}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  \centering{
    $
    \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
    $
  }
  \vspace{0.9cm}
}
\end{minipage}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \centering{
    \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
    \AxiomC{$\myjud{\mytmm}{\mytya}$}
    \AxiomC{$\myjud{\mytmn}{\mytya}$}
    \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
    \DisplayProof

    \myderivsp

    \begin{tabular}{cc}
      \AxiomC{\phantom{$\myctx P \mytyp_l$}}
      \noLine
      \UnaryInfC{$\myjud{\mytmt}{\mytya}$}
      \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\mytmt \mypeq{\mytya} \mytmt}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}}$}
      \noLine
      \UnaryInfC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.2cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}$}
      \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
      \DisplayProof
    \end{tabular}
  }
}

To express equality between two terms inside ITT, the obvious way to do so is
to have the equality construction to be a type-former.  Here we present what
has survived as the dominating form of equality in systems based on ITT up to
the present day.

Our type former is $\mypeq{\mytya}$, which given a type (in this case
$\mytya$) relates equal terms of that type.  $\mypeq{}$ has one introduction
rule, $\myrefl$, which introduces an equality relation between definitionally
equal terms---in the typing rule we display the term as `the same', meaning
`the same up to $\mydefeq$'. % TODO maybe mention this earlier

Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$.  $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
\begin{itemize}
\item $\myse{P}$, a predicate working with two terms of a certain type (say
  $\mytya$) and a proof of their equality
\item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
  $\myse{n}$) are equal
\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
  the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
\end{itemize}
Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
$\mytmm$, $\mytmn$, and $\myse{q}$.  In other words $\myjeqq$ takes a
witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
returns a witness of $\myse{P}$ working with \emph{propositionally equal}
terms.  Invokations of $\myjeqq$ will vanish when the equality proofs will
reduce to invocations to reflexivity, at which point the arguments must be
definitionally equal, and thus the provided
$\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
can be returned.

While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
`friendly' rules from it, for example a more obvious `substitution' rule, that
replaces equal for equal in predicates:
\[
\begin{array}{l}
(\myabs{\myb{A}\ \myb{P}\ \myb{x}\ \myb{y}\ \myb{q}\ \myb{p}}{
  \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{q}}{\myb{p}}}) : \\
\myind{1} \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}}
\end{array}
\]
This rule is often called $\myfun{subst}$---here we will invoke it without
specifying the type ($\myb{A}$) and the sides of the equality
($\myb{x},\myb{y}$).

Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
equality, such as symmetry, transitivity, and a congruence law:

% TODO finish this

\subsection{Common extensions}

eta law

congruence

UIP

\subsection{Limitations}

\epigraph{\emph{Half of my time spent doing research involves thinking up clever
  schemes to avoid needing functional extensionality.}}{@larrytheliquid}

However, propositional equality as described is quite restricted when
reasoning about equality beyond the term structure, which is what definitional
equality gives us (extension notwithstanding).

The problem is best exemplified by \emph{function extensionality}.  In
mathematics, we would expect to be able to treat functions that give equal
output for equal input as the same.  When reasoning in a mechanised framework
we ought to be able to do the same: in the end, without considering the
operational behaviour, all functions equal extensionally are going to be
replaceable with one another.

However this is not the case, or in other words with the tools we have we have
no term of type
\[
\myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
    \myb{A} \myarr \myb{B}}{
        (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
        \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
    }
}
\]
To see why this is the case, consider the functions
\[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\]
where $\myfun{+}$ is defined by recursion on the first argument, gradually
destructing it to build up successors of the second argument.  The two
functions are clearly denotationally the same, and we can in fact prove that
\[
\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
\]
By analysis on the $\myb{x}$.  However, the two functions are not
definitionally equal, and thus we won't be able to get rid of the
quantification.

For the reasons above, theories that offer a propositional equality similar to
what we presented are called \emph{intensional}, as opposed to
\emph{extensional}.  Most systems in wide use today (such as Agda, Coq and
Epigram) are of this kind.

This is quite an annoyance that often makes reasoning awkward to execute.  It
also extends to other fields, for example proving bisimulation between
processes specified by coinduction, or in general proving equivalences based
on the behaviour on a term.

\subsection{Equality reflection}

One way to `solve' this problem is by identifying propositional equality with
definitional equality:

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \centering{
    \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
    \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
    \DisplayProof
  }
}

This rule takes the name of \emph{equality reflection}, and is a very
different rule from the ones we saw up to now: it links a typing judgement
internal to the type theory to a meta-theoretic judgement that the type
checker uses to work with terms.  It is easy to see the dangerous consequences
that this causes:
\begin{itemize}
\item The rule is syntax directed, and the type checker is presumably expected
  to come up with equality proofs when needed.
\item More worryingly, type checking becomes undecidable also because
  computing under false assumptions becomes unsafe.
  Consider for example
  \[
  \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
  \]
  Using the assumed proof in tandem with equality reflection we could easily
  write a classic Y combinator, sending the compiler into a loop.
\end{itemize}

Given these facts theories employing equality reflection, like NuPRL
\citep{NuPRL}, carry the derivations that gave rise to each typing judgement
to keep the systems manageable.  % TODO more info, problems with that.

For all its faults, equality reflection does allow us to prove extensionality,
using the extensions we gave above.  Assuming that $\myctx$ contains
\[\myb{A}, \myb{B} : \mytyp; \myb{f}, \myb{g} : \myb{A} \myarr \myb{B}; \myb{q} : \myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\]
We can then derive
\begin{prooftree}
  \AxiomC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}$}
  \RightLabel{equality reflection}
  \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
  \RightLabel{congruence for $\lambda$s}
  \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
  \RightLabel{$\eta$-law for $\lambda$}
  \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$}
  \RightLabel{$\myrefl$}
  \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
\end{prooftree}

Now, the question is: do we need to give up well-behavedness of our theory to
gain extensionality?

\subsection{Observational equality}
\ref{sec:ott}

% TODO should we explain this in detail?
A recent development by \citet{Altenkirch2007}, \emph{Observational Type
  Theory} (OTT), promises to keep the well behavedness of ITT while being able
to gain many useful equality proofs\footnote{It is suspected that OTT gains
  \emph{all} the equality proofs of ETT, but no proof exists yet.}, including
function extensionality.  The main idea is to give the user the possibility to
\emph{coerce} (or transport) values from a type $\mytya$ to a type $\mytyb$,
if the type checker can prove structurally that $\mytya$ and $\mytya$ are
equal; and providing a value-level equality based on similar principles.  A
brief overview is given below,

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \dots \\
             &  |  & \myprdec{\myprsyn} \mysynsep
                     \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
                     \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
    \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
                     \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\
             &  |  & \mytmsyn = \mytmsyn \mysynsep
                     \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
  \end{array}
  $
}
\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
  \centering{
  }
}

The original presentation of OTT employs the theory presented above.  It is
close to the one presented in section \ref{sec:itt}, with the additions
presented above, and the change that only one the `first' universe, the type
of small types ($\mytyp_0$), is present.

The propositional universe is meant to be where equality proofs live in.  The
equality proofs are respectively between types ($\mytya = \mytyb$), and
between values 



However, only one universe is present ($\mytyp_0$), and a \emph{propositional}
universe is isolated, intended to be the universe where equality proofs live
in.  Propositions (as long as our system is consistent) are inhabited only by
one element, and thus can all be treated as definitionally equal.



\section{Augmenting ITT}
\label{sec:practical}

\subsection{A more liberal hierarchy}

\subsection{Type inference}

\subsubsection{Bidirectional type checking}

\subsubsection{Pattern unification}

\subsection{Pattern matching and explicit fixpoints}

\subsection{Induction-recursion}

\subsection{Coinduction}

\subsection{Dealing with partiality}

\subsection{Type holes}

\section{\mykant}
\label{sec:kant}

\mykant is an interactive theorem prover developed as part of this thesis.
The plan is to present a core language which would be capable of serving as
the basis for a more featureful system, while still presenting interesting
features and more importantly observational equality.

The author learnt the hard way the implementations challenges for such a
project, and while there is a solid and working base to work on, observational
equality is not currently implemented.  However, a detailed plan on how to add
it this functionality is provided, and should not prove to be too much work.

\subsection{High level overview}

\subsubsection{Features}

The features currently implemented in \mykant are:

\begin{description}
\item[Full dependent types] As we would expect, we have dependent a system
  which is as expressive as the `best' corner in the lambda cube described in
  section \ref{sec:itt}.

\item[Implicit, cumulative universe hierarchy] The user does not need to
  specify universe level explicitly, and universes are \emph{cumulative}.

\item[User defined data types and records] Instead of forcing the user to
  choose from a restricted toolbox, we let her define inductive data types,
  with associated primitive recursion operators; or records, with associated
  projections for each field.

\item[Bidirectional type checking] While no `fancy' inference via unification
  is present, we take advantage of an type synthesis system in the style of
  \cite{Pierce2000}, extending the concept for user defined data types.

\item[Type holes] When building up programs interactively, it is useful to
  leave parts unfinished while exploring the current context.  This is what
  type holes are for.
\end{description}

The planned features are:

\begin{description}
\item[Observational equality] As described in section \label{sec:ott} but
  extended to work with the type hierarchy and to admit equality between
  arbitrary data types.

\item[Coinductive data] ...
\end{description}

We will analyse the features one by one, along with motivations and tradeoffs
for the design decisions made.

\subsubsection{Implementation}

The codebase consists of around 2500 lines of Haskell, as reported by the
\texttt{cloc} utility.  The high level design is heavily inspired by Conor
McBride's work on various incarnations of Epigram, and specifically by the
first version as described \citep{McBride2004} and the codebase for the new
version \footnote{Available intermittently as a \texttt{darcs} repository at
  \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}.  In many ways \mykant is
something in between the first and second version of Epigram.

The interaction happens in a read-eval-print loop (REPL).  The repl is a
available both as a commandline application and in a web interface, which is
available at \url{kant.mazzo.li} and presents itself as in figure
\ref{fig:kant-web}.

\begin{figure}
  \centering{
    \includegraphics[scale=1.0]{kant-web.png}
  }
  \caption{The \mykant web prompt.}
  \label{fig:kant-web}
\end{figure}

The interaction with the user takes place in a loop living in and updating a
context \mykant declarations.  The user inputs a new declaration that goes
through various stages starts with the user inputing a \mykant declaration,
which then goes through various stages that can end up in a context update, or
in failures of various kind.  The process is described in figure
\ref{fig:kant-process}.  The workings of each phase will be illustrated in the
next sections.

\begin{figure}
  {\small
  \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
  corners, minimum height=2.5em, node distance=0.7cm]

  \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
  centered, inner sep=0pt, node distance=0.7cm]

  \tikzstyle{line} = [draw, -latex']

  \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
  centered, node distance=1.5cm]


  \begin{tikzpicture}[auto]
    \node [cloud] (user) {User};
    \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
    \node [block, below=of parse] (desugar) {Desugar};
    \node [block, below=of desugar] (reference) {Reference};
    \node [block, below=of reference] (elaborate) {Elaborate};
    \node [block, below=of elaborate] (tycheck) {Typecheck};
    \node [decision, right=of elaborate] (error) {Error?};
    \node [block, right=of parse] (distill) {Distill};
    \node [block, right=of desugar] (update) {Update context};

    \path [line] (user) -- (parse);
    \path [line] (parse) -- (desugar);
    \path [line] (desugar) -- (reference);
    \path [line] (reference) -- (elaborate);
    \path [line] (elaborate) edge[bend right] (tycheck);
    \path [line] (tycheck) edge[bend right] (elaborate);
    \path [line] (elaborate) -- (error);
    \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
    \path [line] (error) -- node [near start] {no} (update);
    \path [line] (update) -- (distill);
    \path [line] (distill) -- (user);
    

  \end{tikzpicture}
  }
  \caption{High level overview of the life of a \mykant prompt cycle.}
  \label{fig:kant-process}
\end{figure}

\subsection{Bidirectional type checking}

We start by describing bidirectional type checking since it calls for fairly
different typing rules that what we have seen up to now.  The idea is to have
two kind of terms: terms for which a type can always be inferred, and terms
that need to be checked against a type.  A nice observation is that this
duality runs through the semantics of the terms: data destructors (function
application, record projections, primitive recursors) \emph{infer} types,
while data constructors (abstractions, record/data types data constructors)
need to be checked.

To introduce the concept and notation, we will revisit the STLC in a
bidirectional style.

\appendix

\section{Notation and syntax}

Syntax, derivation rules, and reduction rules, are enclosed in frames describing
the type of relation being established and the syntactic elements appearing,
for example

\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  \centering{Typing derivations here.}
}

In the languages presented and Agda code samples I also highlight the syntax,
following a uniform color and font convention:

\begin{center}
  \begin{tabular}{c | l}
    $\mytyc{Sans}$   & Type constructors. \\
    $\mydc{sans}$    & Data constructors. \\
    % $\myfld{sans}$  & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
    $\mysyn{roman}$  & Keywords of the language. \\
    $\myfun{roman}$  & Defined values and destructors. \\
    $\myb{math}$     & Bound variables.
  \end{tabular}
\end{center}

Moreover, I will from time to time give examples in the Haskell programming
language as defined in \citep{Haskell2010}, which I will typeset in
\texttt{teletype} font.  I assume that the reader is already familiar with
Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.

When presenting grammars, I will use a word in $\mysynel{math}$ font
(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
element.  More specifically, terms are usually indicated by lowercase letters
(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
$\mytya$, $\mytyb$, or $\mytycc$).

When presenting type derivations, I will often abbreviate and present multiple
conclusions, each on a separate line:

\begin{prooftree}
  \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
  \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
  \noLine
  \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
\end{prooftree}

\section{Agda rendition of core ITT}
\label{app:agda-code}

\begin{code}
module ITT where
  open import Level

  data ⊥ : Set where

  absurd : ∀ {a} {A : Set a} → ⊥ → A
  absurd ()

  record ⊤ : Set where
    constructor tt

  record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
    constructor _,_
    field
      fst  : A
      snd  : B fst

  data Bool : Set where
    true false : Bool

  if_then_else_ : ∀ {a} {P : Bool → Set a} (x : Bool) → P true → P false → P x
  if true then x else _ = x
  if false then _ else x = x

  data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
    _◁_ : (s : S) → (P s → W S P) → W S P

  rec : ∀ {a b} {S : Set a} {P : S → Set b}
    (C : W S P → Set) →       -- some conclusion we hope holds
    ((s : S) →                -- given a shape...
     (f : P s → W S P) →      -- ...and a bunch of kids...
     ((p : P s) → C (f p)) →  -- ...and C for each kid in the bunch...
     C (s ◁ f)) →             -- ...does C hold for the node?
    (x : W S P) →             -- If so, ...
    C x                       -- ...C always holds.
  rec C c (s ◁ f) = c s f (λ p → rec C c (f p))

  data _≡_ {a} {A : Set a} : A → A → Set a where
    refl : ∀ x → x ≡ x

  J : ∀ {a b} {A : Set a}
    (P : (x y : A) → x ≡ y → Set b) →
    ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
  J P p (refl x) = p

  subst : ∀ {a b} {A : Set a}
    (P : A → Set b) →
    ∀ {x y} → (x≡y : x ≡ y) → P x → P y
  subst P q p = J (λ _ y _ → P y) p q
\end{code}

\nocite{*}
\bibliographystyle{authordate1}
\bibliography{thesis}

\end{document}