\usepackage{graphicx}
\usepackage{subcaption}
+% Unicode
+\usepackage{ucs}
+\usepackage[utf8x]{inputenc}
+% \usepackage{autofe}
+
%% -----------------------------------------------------------------------------
%% Fonts
%% \usepackage[osf]{libertine}
%% -----------------------------------------------------------------------------
%% Symbols
-\usepackage{amssymb,amsmath}
+\usepackage[fleqn]{amsmath}
+\usepackage{amssymb}
\usepackage{wasysym}
\usepackage{turnstile}
\usepackage{centernot}
\usepackage{umoline}
\usepackage[export]{adjustbox}
\usepackage{multicol}
+\usepackage{listingsutf8}
+\lstset{
+ basicstyle=\small\ttfamily,
+ extendedchars=\true,
+ inputencoding=utf8x,
+ xleftmargin=1cm
+}
+\usepackage{epigraph}
+
+%% -----------------------------------------------------------------------------
+%% Bibtex
+\usepackage{natbib}
%% Numbering depth
%% \setcounter{secnumdepth}{0}
breaklinks=true,
bookmarks=true,
pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
- pdftitle={The Paths Towards Observational Equality},
+ pdftitle={Observational Equality},
colorlinks=false,
pdfborder={0 0 0}
}
% Make links footnotes instead of hotlinks:
-\renewcommand{\href}[2]{#2\footnote{\url{#1}}}
+% \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
% avoid problems with \sout in headers with hyperref:
\pdfstringdefDisableCommands{\renewcommand{\sout}{}}
-\title{The Paths Towards Observational Equality}
-\author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
+\title{Observational Equality}
+\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{December 2012}
\begin{document}
\maketitle
+\setlength{\tabcolsep}{12pt}
+
+\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.
-In the next sections I will give a very brief overview of STLC, and then
-describe how to augment it to reach the theory I am interested in,
-Inutitionistic Type Theory (ITT), also known as Martin-L\"{o}f Type Theory after
-its inventor.
+Section \ref{sec:types} I 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:practical} will describe additions common in practical programming
+languages based on ITT.
+
+Finally, I will explain why equality has been a tricky business in these
+theories, and talk about the various attempts have been made to make the
+situation better. One interesting development has recently emerged:
+Observational Type theory. I propose to explore the ways to turn these ideas
+into useful practices for programming and theorem proving.
+\end{abstract}
-I will then explain why equality has been a tricky business in this theories,
-and talk about the various attempts have been made. One interesting development
-has recently emerged: Observational Type theory. I propose to explore the ways
-to turn these ideas into useful practices for programming and theorem proving.
+\tableofcontents
\section{Simple and not-so-simple types}
+\label{sec:types}
+
+\subsection{A note on notation}
+
+\newcommand{\appsp}{\hspace{0.07cm}}
+\newcommand{\app}[2]{#1\appsp#2}
+\newcommand{\absspace}{\hspace{0.03cm}}
+\newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2}
+\newcommand{\termt}{t}
+\newcommand{\termm}{m}
+\newcommand{\termn}{n}
+\newcommand{\termp}{p}
+\newcommand{\termf}{f}
+\newcommand{\separ}{\ \ |\ \ }
+\newcommand{\termsyn}{\mathit{term}}
+\newcommand{\axname}[1]{\textbf{#1}}
+\newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}}
+\newcommand{\lcsyn}[1]{\mathrm{\underline{#1}}}
+\newcommand{\lccon}[1]{\mathsf{#1}}
+\newcommand{\lcfun}[1]{\mathbf{#1}}
+\newcommand{\tyarr}{\to}
+\newcommand{\tysyn}{\mathit{type}}
+\newcommand{\ctxsyn}{\mathit{context}}
+\newcommand{\emptyctx}{\cdot}
+
+In the following sections I will introduce a lot of syntax, typing, and
+reduction rules, along with examples. To make the exposition clearer, usually
+the rules are preceded by what the rule looks like and what it shows (for
+example \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}).
+
+In the languages presented I will also use different fonts for different things:
+\begin{tabular}{c | l}
+ $\lccon{Sans}$ & Sans serif, capitalised, for type constructors. \\
+ $\lccon{sans}$ & Sans serif, not capitalised, for data constructors. \\
+ $\lcsyn{roman}$ & Roman, underlined, for the syntax of the language. \\
+ $\lcfun{roman}$ & Roman, bold, for defined functions and values. \\
+ $math$ & Math mode font for quantified variables and syntax elements.
+\end{tabular}
+
+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{typewriter} font. I assume that the reader is already familiar with
+Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
\subsection{Untyped $\lambda$-calculus}
Along with Turing's machines, the earliest attempts to formalise computation
-lead to the $\lambda$-calculus. This early programming language encodes
-computation with a minimal sintax and most notably no ``data'' in the
+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.
The syntax of $\lambda$-terms consists of just three things: variables,
abstractions, and applications:
-\newcommand{\appspace}{\hspace{0.07cm}}
-\newcommand{\app}[2]{#1\appspace#2}
-\newcommand{\abs}[2]{\lambda #1. #2}
-\newcommand{\termt}{\mathrm{T}}
-\newcommand{\termm}{\mathrm{M}}
-\newcommand{\termn}{\mathrm{N}}
-\newcommand{\termp}{\mathrm{P}}
-\newcommand{\separ}{\ |\ }
+\begin{center}
+\axname{syntax}
+$$
+\begin{array}{rcl}
+ \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\
+ x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
+\end{array}
+$$
+\end{center}
-\begin{eqnarray*}
- \termt & ::= & x \separ (\abs{x}{\termt}) \separ (\app{\termt}{\termt}) \\
- x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
-\end{eqnarray*}
% I will omit parethesis in the usual manner. %TODO explain how
-Intuitively, abstractions ($\abs{x}{\termt}$) introduce functions with a named
-parameter ($x$), and applications ($\app{\termt}{\termm}$) apply a function
-($\termt$) to an argument ($\termm$).
+I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
+for variables. I will also assume that all variable names in a term are unique
+to avoid problems with name capturing. Intuitively, abstractions
+($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
+applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
+($\termm$).
-The ``applying'' is more formally explained with a reduction rule:
+The `applying' is more formally explained with a reduction rule:
-\newcommand{\bred}{\to_{\beta}}
+\newcommand{\bred}{\leadsto}
+\newcommand{\bredc}{\bred^*}
-\begin{eqnarray*}
- \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
- \termt \bred \termm & \Rightarrow & \left \{
- \begin{array}{l}
- \app{\termt}{\termn} \bred \app{\termm}{\termn} \\
- \app{\termn}{\termt} \bred \app{\termn}{\termm} \\
- \abs{x}{\termt} \bred \abs{x}{\termm}
- \end{array}
- \right.
-\end{eqnarray*}
+\begin{center}
+\axdesc{reduction}{\termsyn \bred \termsyn}
+$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$
+\end{center}
Where $\termt[\termm / x]$ expresses the operation that substitutes all
-occurrences of $x$ with $\termm$ in $\termt$.
-
-% % TODO put the trans closure
+occurrences of $x$ with $\termm$ in $\termt$. In the future, I will use
+$[\termt]$ as an abbreviation for $[\termt / x]$. In the systems presented, the
+$\bred$ relation also includes reduction of subterms, for example if $\termt
+\bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on.
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):
-\begin{equation*}
- \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dots
-\end{equation*}
+(`loops' in imperative terms):
+\[
+ \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb
+\]
Terms that can be reduced only a finite number of times (the non-looping ones)
-are said to be \emph{normalising}, and the ``final'' term is called \emph{normal
- form}. These concepts (reduction and normal forms) will run through all the
-material analysed.
+are said to be \emph{normalising}, and the `final' term (where no reductions are
+possible on the term or on its subterms) is called \emph{normal form}.
\subsection{The simply typed $\lambda$-calculus}
-\newcommand{\tya}{\mathrm{A}}
-\newcommand{\tyb}{\mathrm{B}}
-\newcommand{\tyc}{\mathrm{C}}
+\newcommand{\tya}{A}
+\newcommand{\tyb}{B}
+\newcommand{\tyc}{C}
-One way to ``discipline'' $\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.
+One way to `discipline' $\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}.
We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
-reads ``in context $\Gamma$, term $\termt$ has type $\tya$''.
+reads `in context $\Gamma$, term $\termt$ has type $\tya$'.
The syntax for types is as follows:
-\newcommand{\tyarr}{\to}
-
-\begin{equation*}
- \tya ::= x \separ \tya \tyarr \tya
-\end{equation*}
+\begin{center}
+ \axname{syntax}
+ $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
+\end{center}
-The $x$ represents all the primitive types that we might want to add to our
-calculus, for example $\mathbb{N}$ or $\mathsf{Bool}$.
+I will use $\tya,\tyb,\dots$ to indicate a generic type.
-A context $\Gamma$ is a map from variables to types. We use the notation
-$\Gamma, x : \tya$ to augment it. Note that, being a map, no variable can
-appear twice as a subject in a context.
+A context $\Gamma$ is a map from variables to types. I will use the notation
+$\Gamma; x : \tya$ to augment it and to `extract' pairs from it.
Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
$\tyb$. We need to be able to decorate our abstractions with
types\footnote{Actually, we don't need to: computers can infer the right type
easily, but that is another story.}:
-\begin{equation*}
- \termt ::= \dots \separ (\abs{x : \tya}{\termt})
-\end{equation*}
+\begin{center}
+ \axname{syntax}
+ $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
+\end{center}
Now we are ready to give the typing judgements:
\begin{center}
- \begin{prooftree}
- \AxiomC{}
- \UnaryInfC{$\Gamma, x : \tya \vdash x : \tya$}
- \end{prooftree}
- \begin{prooftree}
- \AxiomC{$\Gamma, x : \tya \vdash \termt : \tyb$}
+ \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c c}
+ \AxiomC{\phantom{1em}}
+ \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
\UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
- \end{prooftree}
- \begin{prooftree}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
\AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
\AxiomC{$\Gamma \vdash \termm : \tya$}
\BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
- \end{prooftree}
+ \DisplayProof
+ \end{tabular}
\end{center}
-This typing system takes the name of ``simply typed lambda calculus'' (STLC),
+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: %TODO add credit to pierce
+systems \citep{Pierce2002}:
\begin{description}
- % TODO the definition of "stuck" thing is wrong
-\item[Progress] A well-typed term is not stuck. With stuck, we mean a compound
- term (not a variable or a value) that cannot be reduced further. In the raw
- $\lambda$-calculus all we have is functions, but if we add other primitive
- types and constructors it's easy to see how things can go bad - for example
- trying to apply a boolean to something.
+\item[Progress] A well-typed term is not stuck - either it is a value or it can
+ take a step according to the evaluation rules. With `value' we mean a term
+ whose subterms (including itself) don't appear to the left of the $\bred$
+ relation.
\item[Preservation] If a well-typed term takes a step of evaluation, then the
resulting term is also well typed.
\end{description}
\app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
\end{equation*}
-\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1. #2}
+\newcommand{\lcfix}[2]{\lcsyn{fix} \appsp #1\absspace.\absspace #2}
This makes the STLC Turing incomplete. We can recover the ability to loop by
adding a combinator that recurses:
-\begin{equation*}
- \termt ::= \dots \separ \lcfix{x : \tya}{\termt}
-\end{equation*}
-\begin{equation*}
- \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x]
-\end{equation*}
+$$
+ \termsyn ::= \dotsb \separ \lcfix{x : \tysyn}{\termsyn}
+$$
\begin{center}
\begin{prooftree}
- \AxiomC{$\Gamma,x : \tya \vdash \termt : \tya$}
+ \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
\UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
\end{prooftree}
\end{center}
-
-However, we will keep STLC without such a facility. In the next section we shall
-see why that is preferable for our needs.
+$$
+ \lcfix{x : \tya}{\termt} \bred \termt[\lcfix{x : \tya}{\termt}]
+$$
+Which will deprive us of normalisation. There is however a price to pay, which
+will be made clear in the next section.
\subsection{The Curry-Howard correspondence}
+\label{sec:curry-howard}
-It turns out that the STLC can be seen a natural deduction system. Terms are
-proofs, and their types are the propositions they prove. This remarkable fact
-is known as the Curry-Howard isomorphism.
+\newcommand{\lcunit}{\lcfun{\langle\rangle}}
-The ``arrow'' ($\to$) type corresponds to implication. If we wished to
-prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tyc
-\tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the
-correct type:
+It turns out that the STLC can be seen a natural deduction system for
+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' ($\to$) type corresponds to implication. If we wish to prove that
+$(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya \tyarr \tyc)$, all we
+need to do is to devise a $\lambda$-term that has the correct type:
\begin{equation*}
\abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
\end{equation*}
That is, function composition. We might want extend our bare lambda calculus
-with a couple of terms to make our natural deduction more pleasant to use. For
-example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
-are conjunctions. We also want to be able to express falsity, and that is done
-by introducing a type inhabited by no terms. If evidence of such a type is
-presented, then we can derive any type, which expresses absurdity.
-
-\newcommand{\lcinl}{\mathsf{inl}\appspace}
-\newcommand{\lcinr}{\mathsf{inr}\appspace}
-\newcommand{\lccase}[3]{\mathsf{case}\appspace#1\appspace#2\appspace#3}
-\newcommand{\lcfst}{\mathsf{fst}\appspace}
-\newcommand{\lcsnd}{\mathsf{snd}\appspace}
+with a couple of terms former to make our natural deduction more pleasant to
+use. For example, tagged unions (\texttt{Either} in Haskell) are disjunctions,
+and tuples (or products) are conjunctions. We also want to be able to express
+falsity ($\bot$): that can done by introducing a type inhabited by no terms. If
+evidence of such a type is presented, then we can derive any type, which
+expresses absurdity. Conversely, truth ($\top$) is the type with just one
+trivial element ($\lcunit$).
+
+\newcommand{\lcinl}{\lccon{inl}\appsp}
+\newcommand{\lcinr}{\lccon{inr}\appsp}
+\newcommand{\lccase}[3]{\lcsyn{case}\appsp#1\appsp\lcsyn{of}\appsp#2\appsp#3}
+\newcommand{\lcfst}{\lcfun{fst}\appsp}
+\newcommand{\lcsnd}{\lcfun{snd}\appsp}
\newcommand{\orint}{\vee I_{1,2}}
\newcommand{\orintl}{\vee I_{1}}
\newcommand{\orintr}{\vee I_{2}}
\newcommand{\andint}{\wedge I}
\newcommand{\andel}{\wedge E_{1,2}}
\newcommand{\botel}{\bot E}
-\newcommand{\lcabsurd}{\mathsf{absurd}\appspace}
+\newcommand{\lcabsurd}{\lcfun{absurd}\appsp}
+\newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp}
-\begin{eqnarray*}
- \termt & ::= & \dots \\
- & | & \lcinl \termt \separ \lcinr \termt \separ \lccase{\termt}{\termt}{\termt} \\
- & | & (\termt , \termt) \separ \lcfst \termt \separ \lcsnd \termt
-\end{eqnarray*}
-\begin{eqnarray*}
- \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
- \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
- \lcfst (\termt , \termm) & \bred & \termt \\
- \lcsnd (\termt , \termm) & \bred & \termm
-\end{eqnarray*}
-\begin{equation*}
- \tya ::= \dots \separ \tya \vee \tya \separ \tya \wedge \tya \separ \bot
-\end{equation*}
+
+\begin{center}
+ \axname{syntax}
+ $$
+ \begin{array}{rcl}
+ \termsyn & ::= & \dotsb \\
+ & | & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
+ & | & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
+ & | & \lcunit \\
+ \tysyn & ::= & \dotsb \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
+ \end{array}
+ $$
+\end{center}
\begin{center}
+ \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
\begin{prooftree}
\AxiomC{$\Gamma \vdash \termt : \tya$}
\RightLabel{$\orint$}
\RightLabel{$\orel$}
\TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
\end{prooftree}
- \begin{prooftree}
+
+ \begin{tabular}{c c}
\AxiomC{$\Gamma \vdash \termt : \tya$}
\AxiomC{$\Gamma \vdash \termm : \tyb$}
\RightLabel{$\andint$}
\BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
- \end{prooftree}
- \begin{prooftree}
+ \DisplayProof
+ &
\AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
\RightLabel{$\andel$}
\UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
\noLine
\UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
- \end{prooftree}
- \begin{prooftree}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
\AxiomC{$\Gamma \vdash \termt : \bot$}
\RightLabel{$\botel$}
- \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : \tya$}
- \end{prooftree}
+ \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \RightLabel{$\top I$}
+ \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
+ \DisplayProof
+ \end{tabular}
+\end{center}
+\begin{center}
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
+ \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
+ \lcfst (\termt , \termm) & \bred & \termt \\
+ \lcsnd (\termt , \termm) & \bred & \termm
+ \end{eqnarray*}
\end{center}
With these rules, our STLC now looks remarkably similar in power and use to the
natural deduction we already know. $\neg A$ can be expressed as $A \tyarr
\bot$. However, there is an important omission: there is no term of the type $A
\vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
-negation).
+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.
+the foundation of the STLC\footnote{There is research to give computational
+ behaviour to classical logic, but I will not touch those subjects.}.
+
+Finally, going back to our $\lcsyn{fix}$ combinator, it's now easy to see how
+we would want to exclude such a thing if we want to use STLC as a logic, since
+it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
+for any $A$! This is a crucial point: in general we wish to have systems that
+do not let the user devise a term of type $\bot$, otherwise our logic will be
+unsound\footnote{Obviously such a term can be present under a $\lambda$.}.
\subsection{Extending the STLC}
-\newcommand{\lctype}{\mathsf{Type}}
-\newcommand{\lcite}[3]{\mathsf{if}\appspace#1\appspace\mathsf{then}\appspace#2\appspace\mathsf{else}\appspace#3}
-\newcommand{\lcbool}{\mathsf{Bool}}
+\newcommand{\lctype}{\lccon{Type}}
+\newcommand{\lcite}[3]{\lcsyn{if}\appsp#1\appsp\lcsyn{then}\appsp#2\appsp\lcsyn{else}\appsp#3}
+\newcommand{\lcbool}{\lccon{Bool}}
+\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
+\newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3}
+\newcommand{\lcexists}[3]{(#1 : #2) \times #3}
The STLC can be made more expressive in various ways. Henk Barendregt
succinctly expressed geometrically how we can expand our type system:
-\begin{equation*}
+$$
\xymatrix@!0@=1.5cm{
& \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
& & \lambda C \ar@{-}[dd]
\lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
& & \lambda P \ar@{-}[ur]
}
-\end{equation*}
+$$
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}$)] In other words, we can
- quantify over types in our type signatures: $(\lambda A : \lctype. \lambda x :
- A. x) : \forall A. A \to A$. The first and most famous instance of this idea
+\item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
+ types in our type signatures: $(\abs{A : \lctype}{\abs{x : A}{x}}) :
+ \lcforallz{A}{A \tyarr A}$. The first and most famous instance of this idea
has been System F. This gives us a 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}}$)] In other
- words, we have type operators: $(\lambda A : \lctype. \lambda R : \lctype. (A \to R) \to R) : \lctype \to \lctype \to \lctype$.
-\item[Types depending on terms (towards $\lambda{P}$)] Also known as ``dependent
- types'', give great expressive power: $(\lambda x :
- \lcbool. \lcite{x}{\mathbb{N}}{\mathbb{Q}}) : \lcbool \to \lctype$.
+\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
+ type operators: $(\abs{A : \lctype}{\abs{R : \lctype}{(A \to R) \to R}}) :
+ \lctype \to \lctype \to \lctype$.
+\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
+ types', give great expressive power: $(\abs{x : \lcbool}{\lcite{x}{\mathbb{N}}{\mathbb{Q}}}) : \lcbool \to \lctype$.
+\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'.
+
+\section{Intuitionistic Type Theory and dependent types}
+\label{sec:itt}
+
+\newcommand{\lcset}[1]{\lccon{Type}_{#1}}
+\newcommand{\lcsetz}{\lccon{Type}}
+\newcommand{\defeq}{\cong}
+
+\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 too impredicative and thus
+inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section
+ \ref{sec:core-tt} 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).
+
+\subsection{A Core 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}.
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & x \\
+ & | & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\
+ & | & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn)_{x.\termsyn} \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
+ & | & \bot \separ \lcabsurd_{\termsyn} \termsyn \\
+ & | & \lcset{n} \\
+ n & \in & \mathbb{N}
+ \end{eqnarray*}
+
+ \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c c}
+ \AxiomC{\phantom{1em}}
+ \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\tya \defeq \tyb$}
+ \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \bot$}
+ \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
+ \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
+ \AxiomC{$\Gamma \vdash \termm : \tya$}
+ \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm ]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$}
+ \BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$}
+ \noLine
+ \UnaryInfC{$\phantom{1em}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
+ \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt ]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\phantom{1em}$}
+ \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
+ \noLine
+ \UnaryInfC{$\phantom{1em}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
+ \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
+ \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm ] \\
+ \lcfst (\termt, \termm) & \bred & \termt \\
+ \lcsnd (\termt, \termm) & \bred & \termm
+ \end{eqnarray*}
+\end{center}
+
+When showing examples types will be omitted when this can be done without loss
+of clarity, for example $\abs{x}{x}$ in place of $\abs{A : \lcsetz}{\abs{x :
+ A}{x}}$. I will also use $\lcsetz$ as $\lcset{0}$.
+
+There are a lot of new factors at play here. The first thing to notice is that
+the separation between types and terms is gone. All we have is terms, that
+include both values (terms of type $\lcset{0}$) and types (terms of type
+$\lcset{n}$, with $n > 0$). This change is reflected in the typing rules.
+While in the STLC values and types are kept well separated (values never go
+`right of the colon'), in ITT types can freely depend on values.
+
+This relation is expressed in the typing rules for $\tyarr$ and $\times$: if a
+function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
+Examples will make this clearer once some base types are added in section
+\ref{sec:base-types}.
+
+$\tyarr$ and $\times$ are at the core of the machinery of ITT:
+
+\begin{description}
+\item[`forall' ($\tyarr$)] is a generalisation of $\tyarr$ in the STLC and
+ expresses universal quantification in our logic. It is often written with a
+ syntax closer to logic, e.g. $\forall x : \tya. \tyb$. In the
+ literature this is also known as `dependent product' and shown as $\Pi$,
+ following the interpretation of functions as infinitary products. I will just
+ call it `dependent function', reserving `product' for $\exists$.
+
+\item[`exists' ($\times$)] is a generalisation of $\wedge$ in the extended STLC
+ of section \ref{sec:curry-howard}, and thus I will call it `dependent
+ product'. Like $\wedge$, it is formed by providing a pair of things. In our
+ logic, it represents existential quantification. Similarly to $\tyarr$, it is
+ always written as $\exists x : \tya. \tyb$.
+
+ For added confusion, in the literature that calls forall $\Pi$, $\exists$ is
+ often named `dependent sum' and shown as $\Sigma$. This is following the
+ interpretation of $\exists$ as a generalised, infinitary $\vee$, where the
+ first element of the pair is the `tag' that determines which type the second
+ element will have.
\end{description}
-All the systems preserve the properties that make the STLC well behaved (some of
-which I haven't mentioned yet). 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'' above.
+Another thing to notice is that types are very `first class': we are free to
+create functions that accept and return types. For this reason we define
+$\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$
+is the reflexive transitive closure of $\bred$; and we treat types that are
+relate according to $\defeq$ as the same. Another way of seeing $\defeq$ is
+this: when we want to compare two types for equality, we reduce them as far as
+possible and then check if they are equal\footnote{Note that when comparing
+ terms we do it up to $\alpha$-renaming. That is, we do not consider
+ relabelling of variables as a difference - for example $\abs{x : A}{x} \defeq
+ \abs{y : A}{y}$.}. This works since not only each term has a normal form (ITT
+is strongly normalising), but the normal form is also unique; or in other words
+$\bred$ is confluent (if $\termt \bredc \termm$ and $\termt \bredc \termn$, then
+there is a $p$ such that $\termm \bredc \termp$ and $\termn \bredc \termp$).
+This measure makes sure that, for instance, $\app{(\abs{x :
+ \lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality is central
+and will be analysed better later.
+
+The theory presented is \emph{stratified}. We have a hierarchy of types
+$\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all
+types', and our theory is predicative. Type-formers like $\tyarr$ and $\times$
+take the least upper bound $\sqcup$ of the contained types. The layers of the
+hierarchy are called `universes'. Theories where $\lcsetz : \lcsetz$ are
+inconsistent due to Girard's paradox \citep{Hurkens1995}, and thus lose their
+well-behavedness. Some impredicativity sometimes has its place, either because
+the theory retain good properties (normalization, consistency, etc.) anyway,
+like in System F and CoC; or because we are at a stage at which we do not care -
+we will see instances in section \ref{foo}
+% TODO put citation here
+
+Note that the Curry-Howard correspondence runs through ITT as it did with the
+STLC with the difference that ITT corresponds to an higher order propositional
+logic.
+
+\subsection{Base Types}
+\label{sec:base-types}
-\section{Intuitionistic Type Theory}
+\newcommand{\lctrue}{\lccon{true}}
+\newcommand{\lcfalse}{\lccon{false}}
+\newcommand{\lcw}[3]{\lccon{W} #1 : #2 \absspace.\absspace #3}
+\newcommand{\lcnode}[4]{#1 \lhd_{#2 . #3} #4}
+\newcommand{\lcnodez}[2]{#1 \lhd #2}
+\newcommand{\lcited}[5]{\lcsyn{if}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{then}\appsp#4\appsp\lcsyn{else}\appsp#5}
+\newcommand{\lcrec}[4]{\lcsyn{rec}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{with}\appsp#4}
+\newcommand{\lcrecz}[2]{\lcsyn{rec}\appsp#1\appsp\lcsyn{with}\appsp#2}
+\newcommand{\AxiomL}[1]{\Axiom$\fCenter #1$}
+\newcommand{\UnaryInfL}[1]{\UnaryInf$\fCenter #1$}
+
+While the ITT presented is a fairly complete logic, it is not that useful for
+programming. If we wish to make it better, we can add some base types to
+represent the data structures we know and love, such as numbers, lists, and
+trees. Apart from some unsurprising data types, we introduce $\lccon{W}$, a
+very general tree-like structure useful to represent inductively defined types
+and that will allow us to express structural recursion in an equally general
+manner.
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & \dots \\
+ & | & \top \separ \lcunit \\
+ & | & \lcbool \separ \lctrue \separ \lcfalse \separ \lcited{\termsyn}{x}{\termsyn}{\termsyn}{\termsyn} \\
+ & | & \lcw{x}{\termsyn}{\termsyn} \separ \lcnode{\termsyn}{x}{\termsyn}{\termsyn} \separ \lcrec{\termsyn}{x}{\termsyn}{\termsyn}
+ \end{eqnarray*}
+
+ \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c c}
+ \AxiomC{}
+ \UnaryInfC{$\hspace{0.2cm}\Gamma \vdash \top : \lcset{0} \hspace{0.2cm}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcbool : \lcset{0}$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
+ \noLine
+ \UnaryInfC{\phantom{1em}}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \termt : \lcbool$}
+ \AxiomC{$\Gamma \vdash \termm : \tya[\lctrue]$}
+ \AxiomC{$\Gamma \vdash \termn : \tya[\lcfalse]$}
+ \TrinaryInfC{$\Gamma \vdash \lcited{\termt}{x}{\tya}{\termm}{\termn} : \tya[\termt]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
+ \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
+ \BinaryInfC{$\Gamma \vdash \lcw{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\Gamma \vdash \termf : \tyb[\termt ] \tyarr \lcw{x}{\tya}{\tyb}$}
+ \BinaryInfC{$\Gamma \vdash \lcnode{\termt}{x}{\tyb}{\termf} : \lcw{x}{\tya}{\tyb}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \termt: \lcw{x}{\tya}{\tyb}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcforall{\termm}{\tya}{\lcforall{\termf}{\tyb[\termm] \tyarr \lcw{x}{\tya}{\tyb}}{(\lcforall{\termn}{\tyb[\termm]}{\tyc[\app{\termf}{\termn}]}) \tyarr \tyc[\lcnodez{\termm}{\termf}]}}$}
+ \UnaryInfC{$\Gamma \vdash \lcrec{\termt}{x}{\tyc}{\termp} : \tyc[\termt]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \lcited{\lctrue}{x}{\tya}{\termt}{\termm} & \bred & \termt \\
+ \lcited{\lcfalse}{x}{\tya}{\termt}{\termm} & \bred & \termm \\
+ \lcrec{\lcnodez{\termt}{\termf}}{x}{\tya}{\termp} & \bred & \app{\app{\app{\termp}{\termt}}{\termf}}{(\abs{\termm}{\lcrec{\app{f}{\termm}}{x}{\tya}{\termp}})}
+ \end{eqnarray*}
+\end{center}
+
+The introduction and elimination for $\top$ and $\lcbool$ are unsurprising.
+Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the
+branches are dependent on the value of the conditional.
+
+% TODO: explain better here
+
+The rules for $\lccon{W}$, on the other hand, are quite an eyesore. The idea
+behind $\lccon{W}$ types is to build up `trees' where the number of `children'
+of each node is dependent on the value in the node. This is captured by the
+$\lhd$ constructor, where the argument on the left is the value, and the
+argument on the right is a function that returns a child for each possible value
+of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The recursor
+$\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that
+$\tyc[\termt]$ holds.
+
+\subsection{Some examples}
+
+Now we can finally provide some meaningful examples. Apart from omitting types,
+I will also use some abbreviations:
+\begin{itemize}
+ \item $\_\mathit{operator}\_$ to define infix operators
+ \item $\abs{x\appsp y\appsp z : \tya}{\dotsb}$ to define multiple abstractions at the same
+ time
+\end{itemize}
+
+\subsubsection{Sum types}
+
+We would like to recover our sum type, or disjunction, $\vee$. This is easily
+achieved with $\times$:
+\[
+\begin{array}{rcl}
+ \_\vee\_ & = & \abs{\tya\appsp\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\
+ \lcinl & = & \abs{x}{(\lctrue, x)} \\
+ \lcinr & = & \abs{x}{(\lcfalse, x)} \\
+ \lcfun{case} & = & \abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\
+ & & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}}
+\end{array}
+\]
+What is going on here? We are using $\exists$ with $\lcbool$ as a tag, so that
+we can choose between one of two types in the second element. In
+$\lcfun{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the
+tag, that is, the first element of $x : \tya \vee \tyb$. If the tag is true,
+then we know that the second element is of type $\tya$, and we will apply $f$.
+The same applies to the other branch, with $\tyb$ and $g$.
+
+\subsubsection{Naturals}
+
+Now it's time to showcase the power of $\lccon{W}$ types.
+\begin{eqnarray*}
+ \lccon{Nat} & = & \lcw{b}{\lcbool}{\lcite{b}{\top}{\bot}} \\
+ \lccon{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\
+ \lccon{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\
+ \lcfun{plus} & = & \abs{x\appsp y}{\lcrecz{x}{(\abs{b}{\lcite{b}{\abs{\_\appsp f}{\app{\lccon{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appsp\_}{y}}})}}
+\end{eqnarray*}
+Here we encode natural numbers through $\lccon{W}$ types. Each node contains a
+$\lcbool$. If the $\lcbool$ is $\lcfalse$, then there are no children, since we
+have a function $\bot \tyarr \lccon{Nat}$: this is our $0$. If it's $\lctrue$,
+we need one child only: the predecessor. We recurse giving $\lcsyn{rec}$ a
+function that handles the `base case' 0 when the $\lcbool$ is $\lctrue$, and the
+inductive case otherwise.
+
+We postpone more complex examples after the introduction of inductive families
+and pattern matching, since $\lccon{W}$ types get unwieldy very quickly.
+
+\subsection{Propositional Equality}
+\label{sec:propeq}
+
+We can finally introduce one of the central subjects of my project:
+propositional equality.
+
+\newcommand{\lceq}[3]{#2 =_{#1} #3}
+\newcommand{\lceqz}[2]{#1 = #2}
+\newcommand{\lcrefl}[2]{\lccon{refl}_{#1}\appsp #2}
+\newcommand{\lcsubst}[3]{\lcfun{subst}\appsp#1\appsp#2\appsp#3}
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & ... \\
+ & | & \lceq{\termsyn}{\termsyn}{\termsyn} \separ \lcrefl{\termsyn}{\termsyn} \separ \lcsubst{\termsyn}{\termsyn}{\termsyn}
+ \end{eqnarray*}
+
+ \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \UnaryInfC{$\Gamma \vdash \lcrefl{\tya}{\termt} : \lceq{\tya}{\termt}{\termt}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termp : \lceq{\tya}{\termt}{\termm}$}
+ \AxiomC{$\Gamma \vdash \tyb : \tya \tyarr \lcsetz$}
+ \AxiomC{$\Gamma \vdash \termn : \app{\tyb}{\termt}$}
+ \TrinaryInfC{$\Gamma \vdash \lcsubst{\termp}{\tyb}{\termn} : \app{\tyb}{\termm}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \lcsubst{(\lcrefl{\tya}{\termt})}{\tyb}{\termm} \bred \termm
+ \end{eqnarray*}
+\end{center}
+
+Propositional equality internalises equality as a type. The only way to
+introduce an equality proof is by reflexivity ($\lccon{refl}$). The eliminator
+is in the style of `Leibnitz's law' of equality: `equals can be substituted for
+equals' ($\lcfun{subst}$). The computation rule refers to the fact that every
+proof of equality will be a $\lccon{refl}$. We can use $\neg
+(\lceq{\tya}{x}{y})$ to express inequality.
+
+These elements conclude our presentation of a `core' type theory. For an
+extended example of a similar theory in use see Section 6.2 of
+\cite{Thompson1991}\footnote{Note that while I attempted to formalise the proof
+ in Agda, I found a bug in the book! See the errata for details:
+ \url{http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/errata.html}.}. The above
+language and examples have been codified in Agda\footnote{More on Agda in the
+ next section.}, see appendix \ref{app:agda-code}.
+
+\section{A more useful language}
+\label{sec:practical}
+
+While our core type theory equipped with $\lccon{W}$ types is very usefully
+conceptually as a simple but complete language, things get messy very fast. In
+this section I will present the elements that are usually included in theorem
+provers or programming languages to make them usable by mathematicians or
+programmers.
+
+All the features presented are present in the second version of the Agda system
+\citep{Norell2007, Bove2009}. Agda follows a tradition of theorem provers based
+on ITT with inductive families and pattern matching. The closest relative of
+Agda, apart from previous versions, is Epigram \citep{McBride2004, EpigramTut}.
+Coq is another notable theorem prover based on the same concepts, and the first
+and most popular \citep{Coq}.
+
+The main difference between Coq and Agda/Epigram is that the former focuses on
+theorem proving, while the latter also want to be useful as functional
+programming languages, while still offering good tools to express
+mathematics\footnote{In fact, currently, Agda is used almost exclusively to
+ express mathematics, rather than to program.}. This is reflected in a series
+of differences that I will not discuss here (most notably the absence of tactics
+but better support for pattern matching in Agda/Epigram). I will take the same
+approach as Agda/Epigram and will give a perspective focused on functional
+programming rather than theorem proving. Every feature will be presented as it
+is Agda.
+
+\subsection{Bidirectional type checking}
+
+Lastly, the theory I present is fully explicit in the sense that the user has to
+specify every type when forming abstractions, products, etc. This can be a
+great burden if one wants to use the theory directly. Complete inference is
+undecidable (which is hardly surprising considering the role that types play)
+but partial inference (also called `bidirectional type checking' in this
+context) in the style of \cite{Pierce2000} will have to be deployed in a
+practical system.
+
+\subsection{Inductive families}
+
+\newcommand{\lcdata}[1]{\lcsyn{data}\appsp #1}
+\newcommand{\lcdb}{\ |\ }
+\newcommand{\lcind}{\hspace{0.2cm}}
+\newcommand{\lcwhere}{\appsp \lcsyn{where}}
+\newcommand{\lclist}[1]{\app{\lccon{List}}{#1}}
+\newcommand{\lcnat}{\lccon{Nat}}
+\newcommand{\lcvec}[2]{\app{\app{\lccon{Vec}}{#1}}{#2}}
+
+Inductive families were first introduced by \cite{Dybjer1991}. For the reader
+familiar with the recent developments present in the GHC compiler for Haskell,
+inductive families will look similar to GADTs (Generalised Abstract Data Types)
+\citep[Section 7.4.7]{GHC}.
+Haskell style data types provide \emph{parametric polymorphism}, so that we can
+define types that range over type parameters:
+\begin{lstlisting}
+List a = Nil | Cons a (List a)
+\end{lstlisting}
+In this way we define the \texttt{List} type once while allowing elements to be
+of any type. In Haskell \texttt{List} will be a type constructor of kind
+\texttt{* -> *}, while \texttt{Nil :: List a} and \texttt{Cons :: a -> List a -> List a}\footnote{Note that the \texttt{a}s are implicitly quantified type variables}.
+
+Inductive families bring this concept one step further by allowing some of the
+parameters to be constrained by constructors. We call these `variable'
+parameters `indices'. For example we might define natural numbers
+\[
+\begin{array}{l}
+\lcdata{\lcnat} : \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{zero} &: \lcnat \\
+ \lcind \lccon{suc} &: \lcnat \tyarr \lcnat
+ \end{array}
+\end{array}
+\]
+And then define a type for lists indexed by length:
+\[
+\begin{array}{l}
+\lcdata{\lccon{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{nil} &: \lcvec{A}{\lccon{zero}} \\
+ \lcind \_::\_ &: \{n : \lccon{Nat}\} \tyarr A \tyarr \lcvec{A}{n} \tyarr \lcvec{A}{\app{(\lccon{suc}}{n})}
+ \end{array}
+\end{array}
+\]
+Note that contrary to the Haskell ADT notation, with inductive families we
+explicitly list the types for the type and data constructors. In $\lccon{Vec}$,
+$A$ is a parameter (same across all constructors) while the $\lcnat$ is an
+index. In our syntax, in the $\lcsyn{data}$ declaration, things to the left of
+the colon are parameters, while on the right we can define the type of indices.
+Also note that the parameters' identifiers will be in scope across all
+constructors, while indices' won't.
+
+In this $\lccon{Vec}$ example, when we form a new list the length is
+$\lccon{zero}$. When we append a new element to an existing list of length $n$,
+the new list is of length $\app{\lccon{suc}}{n}$, that is, one more than the
+previous length. Also note that we are using the $\{n : \lcnat\} \tyarr \dotsb$
+syntax to indicate an argument that we will omit when using $\_::\_$. In the
+future I shall also omit the type of these implicit parameters, in line with how
+Agda works.
+
+Once we have $\lccon{Vec}$ we can do things much more safely than with normal
+lists. For example, we can define an $\lcfun{head}$ function that returns the
+first element of the list:
+\[
+\begin{array}{l}
+\lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A
+\end{array}
+\]
+Note that we will not be able to provide this function with a
+$\lcvec{A}{\lccon{zero}}$, since it needs an index which is a successor of some
+number.
+
+\newcommand{\lcfin}[1]{\app{\lccon{Fin}}{#1}}
+
+If we wish to index a $\lccon{Vec}$ safely, we can define an inductive family
+$\lcfin{n}$, which represents the family of numbers smaller than a given number
+$n$:
+\[
+\begin{array}{l}
+ \lcdata{\lccon{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{fzero} &: \{n\} \tyarr \lcfin{(\app{\lccon{suc}}{n})} \\
+ \lcind \lccon{fsuc} &: \{n\} \tyarr \lcfin{n} \tyarr \lcfin{(\app{\lccon{suc}}{n})}
+ \end{array}
+\end{array}
+\]
+$\lccon{fzero}$ is smaller than any number apart from $\lccon{zero}$. Given
+the family of numbers smaller than $n$, we can produce the family of numbers
+smaller than $\app{\lccon{suc}}{n}$. Now we can define an `indexing' operation
+for our $\lccon{Vec}$:
+\[
+\begin{array}{l}
+\_\lcfun{!!}\_ : \{A\ n\} \tyarr \lcvec{A}{n} \tyarr \lcfin{n} \tyarr A
+\end{array}
+\]
+In this way we will be sure that the number provided as an index will be smaller
+than the length of the $\lccon{Vec}$ provided.
+
+\subsubsection{Computing with inductive families}
+
+I have carefully avoided to define the functions that I mentioned as example,
+since one question still is unanswered: `how do we work with inductive
+families'? The most basic approach is to work with eliminators, that can be
+automatically provided by the programming language for each data type defined.
+For example the induction principle on natural numbers will serve as an
+eliminator for $\lcnat$:
+\[
+\begin{array}{l@{\ } c@{\ } l}
+ \lcfun{NatInd} & : & (A : \lcsetz) \tyarr \\
+ & & A \tyarr (\lcnat \tyarr A \tyarr A) \tyarr \\
+ & & \lcnat \tyarr A
+\end{array}
+\]
+
+That is, if we provide an $A$ (base case), and then given a number and an $A$ we
+give the next $A$ (inductive step), then an $A$ can be computed for every
+number. This can be expressed easily in Haskell:
+\begin{lstlisting}
+data Nat = Zero | Suc Nat
+natInd :: a -> (Nat -> a -> a) -> Nat -> a
+natInd z _ Zero = z
+natInd z f (Suc n) = f n (natInd z f n)
+\end{lstlisting}
+However, in a dependent setting, we can do better:
+\[
+\begin{array}{l@{\ } c@{\ } l}
+ \lcfun{NatInd} & : & (P : \lcnat \tyarr \lcsetz) \tyarr \\
+ & & \app{P}{\lccon{zero}} \tyarr ((n : \lcnat) \tyarr \app{P}{n} \tyarr \app{P}{(\app{\lccon{suc}}{n})}) \tyarr \\
+ & & (n : \lcnat) \tyarr \app{P}{n}
+\end{array}
+\]
+This expresses the fact that the resulting type can be dependent on the number.
+In other words, we are proving that $P$ holds for all $n : \lcnat$.
+
+Naturally a reduction rule will be associated with each eliminator:
+$$
+\begin{array}{l c l}
+\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{\lccon{zero}} & \bred & z \\
+\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{(\app{\lccon{suc}}{n})} & \bred & \app{\app{f}{n}}{(\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{n})}
+\end{array}
+$$
+Which echoes the \texttt{natInd} function defined in Haskell. An extensive
+account on combinators and inductive families can be found in \cite{McBride2004}.
+
+\subsubsection{Pattern matching and guarded recursion}
+
+However, combinators are far more cumbersome to use than the techniques usually
+employed in functional programming: pattern matching and recursion.
+\emph{General} recursion cannot be added if we want to keep our theory free of
+$\bot$. The common solution to this problem is to allow recursive calls only if
+the arguments are structurally smaller than what the function received. Pattern
+matching on the other hand gains considerable power with inductive families,
+since when we match a constructor we are gaining information on the indices of
+the family. Thus matching constructors will enable us to restrict patterns of
+other arguments.
+
+Following this discipline defining $\lcfun{head}$ becomes easy:
+\[
+\begin{array}{l}
+\lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A \\
+\lcfun{head}\appsp(x :: \_) = x
+\end{array}
+\]
+We need no case for $\lccon{nil}$, since the type checker knows that the
+equation $n = \lccon{zero} = \app{\lccon{suc}}{n'}$ cannot be satisfied.
+
+More details on the implementations of inductive families can be found in
+\citep{McBride2004, Norell2007}.
+
+\subsection{Friendlier universes}
+
+Universes as presented in section \ref{sec:core-tt} are quite cumbersome to work
+with. Consider the example where we define an inductive family for booleans and
+then we want to define an `if then else' eliminator:
+\[
+\begin{array}{l}
+\lcdata{\lcbool} : \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{true} &: \lcbool \\
+ \lcind \lccon{false} &: \lcbool
+ \end{array}\\
+\\
+\lcfun{ite} : \{A : \lcset{0}\} \tyarr \lcbool \tyarr A \tyarr A \tyarr A \\
+\lcfun{ite} \appsp \lccon{true} \appsp x \appsp \_ = x \\
+\lcfun{ite} \appsp \lccon{false} \appsp \_ \appsp x = x
+\end{array}
+\]
+
+What if we want to use $\lcfun{ite}$ with types, for example $\lcfun{ite} \appsp
+b \appsp \lcnat \appsp \lccon{Bool}$? Clearly $\lcnat$ is not of type
+$\lcset{0}$, so we'd have to redefine $\lcfun{ite}$ with exactly the same body,
+but different type signature. The problem is even more evident with type
+families: for example our $\lccon{List}$ can only contain values, and if we want
+to build lists of types we need to define another identical, but differently
+typed, family.
+
+One option is to have a \emph{cumulative} theory, where $\lcset{n} : \lcset{m}$
+iff $n < m$. Then we can have a sufficiently large level in our type signature
+and forget about it. Moreover, levels in this setting can be inferred
+mechanically \citep{Pollack1990}, and thus we might lift the burden of universes
+from the user. This is the approach taken by Epigram.
+
+Another more expressive (but currently more cumbersome) way is to expose
+universes more, giving the user a way to quantify them and to take the least
+upper bound of two levels. This is the approach taken by Agda, where for
+example we can define a level-polymorphic $\times$:
+\[
+\begin{array}{l}
+\lcdata{\_\times\_}\ \{a\ b : \lccon{Level}\}\ (A : \lcset{a})\ (B : A \tyarr \lcset{b}) : \lcset{a \sqcup b} \lcwhere \\
+ \lcind \_ , \_ : (x : A) \tyarr \app{B}{x} \tyarr A \times \app{B}{x}
+\end{array}
+\]
+Levels can be made implicit as shown and can be almost always inferred.
+However, having to decorate each type signature with quantified levels adds
+quite a lot of noise. An inference algorithm that automatically quantifies and
+instantiates levels (much like Hindley-Milner for types) seems feasible, but
+currently not implemented anywhere.
+
+\subsection{Coinduction}
+
+One thing that the Haskell programmer will miss in ITT as presented is the
+possibility to work with infinite data. The classic example is the manipulation
+of infinite streams:
+\begin{lstlisting}
+zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
+
+fibs :: [Int]
+fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
+\end{lstlisting}
+While we can clearly write useful programs of this kind, we need to be careful,
+since \texttt{length fibs}, for example, does not make much sense\footnote{Note
+ that if instead of machine \texttt{Int}s we used naturals as defined
+ previously, getting the length of an infinite list would a productive
+ definition.}.
+
+In less informal terms, we need to distinguish between \emph{productive} and
+non-productive definitions. A productive definition is one for which pattern
+matching on data will never diverge, which is the case for \texttt{fibs} but
+not, for example, for \texttt{let x = x in x :: [Int]}. It is very desirable to
+recover \emph{only} the productive definition so that total programs working
+with infinite data can be written.
+
+This desire has lead to work on coindunction
+% TODO finish
+
+\section{Many equalities}
+
+\subsection{Revision, and function extensionality}
+
+\epigraph{\emph{Half of my time spent doing research involves thinking up clever
+ schemes to avoid needing functional extensionality.}}{@larrytheliquid}
+
+Up to this point, I have introduced two equalities: \emph{definitional} equality
+($\defeq$) and \emph{propositional} equality ($=_{\tya}$).
+
+Definitional equality relates terms that the type checker identifies as equal.
+Our definition in section \ref{sec:core-tt} consisted of `reduce the two terms
+to their normal forms, then check if they are equal (up to $\alpha$-renaming)'.
+We can extend this definition in other ways so that more terms will be
+identified as equal. Common ones include doing $\eta$-expansion, which converts
+partial appications of functions, and congruence laws for $\lambda$:
+\begin{center}
+ \begin{tabular}{c c c}
+ \AxiomC{$\Gamma \vdash \termf : \tya \tyarr \tyb$}
+ \UnaryInfC{$\Gamma \vdash \termf \defeq \abs{x}{\app{\termf}{x}}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma; x : \tya \vdash \termf \defeq g$}
+ \UnaryInfC{$\Gamma \vdash \abs{x}{\termf} \defeq \abs{x}{g}$}
+ \DisplayProof
+ \end{tabular}
+\end{center}
+Definitional equality is used in the type checking process, and this means that
+in dependently typed languages type checking and evaluation are intertwined,
+since we need to reduce types to normal forms to check if they are equal. It
+also means that we need be able to compute under binders, for example to
+determine that $\abs{x}{\app{(\abs{y}{y})}{\tya}} \defeq \abs{x}{\tya}$. This
+process goes on `under the hood' and is outside the control of the user.
+
+Propositional equality, on the other hand, is available to the user to reason
+about equality, internalising it as a type. As we have seen in section
+\ref{sec:propeq} propositional equality is introduced by reflexivity and
+eliminated with a `Leibnitz's law' style rule ($\lcfun{subst}$). Now that we
+have inductive families and dependent pattern matching we do not need hard coded
+rules to express this concepts\footnote{Here I use Agda notation, and thus I
+ cannot redefine $=$ and use subscripts, so I am forced to use $\equiv$ with
+ implicit types. After I will carry on using the old notation.}:
+\[
+\begin{array}{l}
+ \lcdata{\lccon{\_\equiv\_}} : \{A : \lcsetz\} : A \tyarr A \tyarr \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{refl} &: \{x : A\} \tyarr x \equiv x
+ \end{array} \\
+ \\
+ \lcfun{subst} : \{A : \lcsetz\} \tyarr \{t\ m : A\} \tyarr t \equiv m \tyarr (B : A \tyarr \lcsetz) \tyarr \app{B}{t} \tyarr \app{B}{m} \\
+ \lcfun{subst} \appsp \lccon{refl}\appsp B \appsp n = n
+\end{array}
+\]
+Here matching $\lccon{refl}$ tells the type checker that $t \defeq m$, and thus
+$\app{B}{t} \defeq \app{B}{m}$, so we can just return $n$.
+
+While propositional equality is a very useful construct, we can prove less terms
+equal than we would like to. For example, if we have the usual functions
+\[
+\begin{array}{l@{\ } l}
+\lcfun{id} & : \{A : \lcsetz\} \tyarr A \tyarr A \\
+\lcfun{map} & : \{A\ B : \lcsetz\} \tyarr (A \tyarr B) \tyarr \app{\lccon{List}}{A} \tyarr \app{\lccon{List}}{B}
+\end{array}
+\]
+we would certainly like to have a term of type
+\[\{A\ B : \lcsetz\} \tyarr
+\app{\lcfun{map}}{\lcfun{id}} =_{\lclist{A} \tyarr \lclist{B}} \lcfun{id}\]
+We cannot do this in ITT, since the things on the sides of $=$ look too
+different at the term level. What we can have is
+\[
+\{A\ B : \lcsetz\} \tyarr (x : \lclist{A}) \tyarr \app{\app{\lcfun{map}}{\lcfun{id}}}{x}
+=_{\lclist{B}} \app{\lcfun{id}}{x}
+\]
+Since the type checker has something to compute with (even if only a variable)
+and reduce the two lists to equal normal forms. The root of this problem is
+that \emph{function extensionality} does not hold:
+\[
+\begin{array}{l@{\ } l}
+\lcfun{ext} : & \{A\ B : \lcsetz\} \tyarr (f\ g : A \tyarr B) \tyarr \\
+ & ((x : A) \tyarr \app{f}{x} =_{A} \app{g}{x}) \tyarr f =_{A \tyarr B} g
+\end{array}
+\]
+Which is a long standing issue in ITT.
+
+\subsection{Extensional Type Theory and its problems}
+
+One way to `solve' the problem and gain extensionality is to allow the type
+checker to derive definitional equality from propositional equality, introducing
+what is known as the `equality reflection' rule:
+\begin{center}
+ \begin{prooftree}
+ \AxiomC{$\Gamma \vdash t =_A m$}
+ \UnaryInfC{$\Gamma \vdash t \defeq m$}
+ \end{prooftree}
+\end{center}
+This jump from types to a metatheoretic relation has deep consequences. But
+firstly, let's get extensionality out of the way. Given $\Gamma = \lcfun{eq} :
+(x : A) \tyarr \app{f}{x} = \app{g}{x}$, we have:
+\begin{center}
+ \begin{prooftree}
+ \AxiomC{$\Gamma; x : A \vdash \app{\lcfun{eq}}{x} : \app{f}{x} = \app{g}{x}$}
+ \RightLabel{(equality reflection)}
+ \UnaryInfC{$\Gamma; x : A \vdash \app{f}{x} \defeq \app{g}{x}$}
+ \RightLabel{(congruence for $\lambda$)}
+ \UnaryInfC{$\Gamma \vdash \abs{x : A}{\app{f}{x}} \defeq \abs{x : A}{\app{g}{x}}$}
+ \RightLabel{($\eta$-law)}
+ \UnaryInfC{$\Gamma \vdash f \defeq g$}
+ \RightLabel{($\lccon{refl}$)}
+ \UnaryInfC{$\Gamma \vdash f = g$}
+ \end{prooftree}
+\end{center}
+Since the above is possible, theories that include the equality reflection rule
+are often called `Extensional Type Theories', or ETTs. A notable exponent of
+this discipline is the NuPRL system \citep{Constable86}. Moreover, equality
+reflection simplifies $\lcfun{subst}$-like operations, since if we have $t = m$
+and $\app{A}{t}$, then by equality reflection clearly $\app{A}{t} \defeq
+\app{A}{m}$.
+
+However equality reflection comes at a great price. The first hit is that it is
+now unsafe to compute under binders, since we can send the type checker into a
+loop given that under binders we can have any equality proof we might want
+(think about what happens with $\abs{x : \bot}{\dotsb}$), and thus we can
+convince the type checker that a term has any type we might want. Secondly,
+equality reflection is not syntax directed, thus the type checker would need to
+`invent' proofs of propositional equality to prove two terms definitionally
+equal, rendering the type checking process undecidable. Thus the type checker
+needs to carry complete derivations for each typing judgement, instead of
+relying on terms only.
+
+\subsection{Observational equality}
+
+A recent development by \cite{Altenkirch2007} promises to keep the well
+behavedness of ITT while being able to gain many useful equality proofs,
+including function extensionality. Starting from a theory similar to the one
+presented in section \ref{sec:itt} but with only $\lcset{0}$, a propositional
+subuniverse of $\lcsetz$ is introduced, plus a `decoding' function:
+
+\newcommand{\lcprop}{\lccon{Prop}}
+
+\begin{center}
+ \begin{tabular}{c c c}
+ \AxiomC{\phantom{1em}}
+ \UnaryInfC{$\Gamma \vdash \lcprop : \lcsetz$}
+ \noLine
+ \UnaryInfC{\phantom{1em}}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{1em}}
+ \UnaryInfC{$\Gamma \vdash \bot : \lcprop$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \top : \lcprop$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash P : \lcprop$}
+ \AxiomC{$\Gamma \vdash Q : \lcprop$}
+ \BinaryInfC{$\Gamma \vdash P \wedge Q : \lcprop$}
+ \noLine
+ \UnaryInfC{\phantom{1em}}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash S : \lcsetz$}
+ \AxiomC{$\Gamma \vdash q : \lcprop$}
+ \BinaryInfC{$\Gamma \vdash p \wedge q : \lcprop$}
+ \noLine
+ \UnaryInfC{\phantom{1em}}
+ \DisplayProof
+ \end{tabular}
+\end{center}
+
+\section{What to do}
+
+
+\bibliographystyle{authordate1}
+\bibliography{background}
+
+\appendix
+\section{Agda code}
+\label{app:agda-code}
+
+\lstset{
+ xleftmargin=0pt
+}
-In this section I will describe
+\lstinputlisting{background.agda}
\end{document}
projects / bitonic-mengthesis.git / blobdiff