...

diff --git a/kant-web.png b/kant-web.png
new file mode 100644 (file)
index 0000000..8a2d329
Binary files /dev/null and b/kant-web.png differ

diff --git a/thesis.lagda b/thesis.lagda
index eb7dc9e0fd65f9c111fecdeb22ffc65127d33727..8a5065c22c2a25d7cb204eb7ba4d8400c4391b2b 100644 (file)
--- a/thesis.lagda
+++ b/thesis.lagda
@@ -14,6 +14,7 @@
 
 %% Symbols
 \usepackage[fleqn]{amsmath}
 
 %% Symbols
 \usepackage[fleqn]{amsmath}

+\usepackage{stmaryrd}           %llbracket

 
 %% Proof trees
 \usepackage{bussproofs}
 
 %% Proof trees
 \usepackage{bussproofs}


@@ -21,6 +22,19 @@
 %% Diagrams
 \usepackage[all]{xy}
 
 %% 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}
 %% -----------------------------------------------------------------------------
 %% Commands for Agda
 \usepackage[english]{babel}


@@ -64,14 +78,23 @@
 
 \FrameSep0.2cm
 \newcommand{\mydesc}[3]{
 
 \FrameSep0.2cm
 \newcommand{\mydesc}[3]{

-  {\small
-    \vspace{0.3cm}
-  \hfill \textbf{#1} $#2$
-  \vspace{-0.3cm}
-  \begin{framed}
-    #3
-  \end{framed}
-}
+  \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?
 }
 
 % TODO is \mathbin the correct thing for arrow and times?


@@ -97,7 +120,7 @@
 % TODO \mathbin or \mathrel here?
 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
 % TODO \mathbin or \mathrel here?
 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
 \newcommand{\mytt}{\mydc{$\langle\rangle$}}

-\newcommand{\myunit}{\mytyc{$\top$}}
+\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{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
 \newcommand{\myfst}{\myfld{fst}}
 \newcommand{\mysnd}{\myfld{snd}}


@@ -108,7 +131,7 @@
 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
 \newcommand{\myright}[1]{\mydc{right}_{#1}}
 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
 \newcommand{\myright}[1]{\mydc{right}_{#1}}

-\newcommand{\myempty}{\mytyc{$\bot$}}
+\newcommand{\myempty}{\mytyc{Empty}}

 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
 \newcommand{\myarg}{\_}
 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
 \newcommand{\myarg}{\_}


@@ -135,6 +158,23 @@
 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
 \newcommand{\mylub}{\sqcup}
 \newcommand{\mydefeq}{\cong}
 \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}}

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


@@ -655,6 +695,20 @@ 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).
 
 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}
 
 \subsection{A simple type theory}
 \label{sec:core-tt}
 


@@ -745,13 +799,20 @@ 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.
 
 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$.  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
+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.
 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.


@@ -760,11 +821,11 @@ 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
 $\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.
+`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}
 % TODO add sectioon about universes
 
 \subsubsection{Contexts}


@@ -981,13 +1042,118 @@ type-level binders, $\myprod$ and $\mytyc{W}$.
    }
 }
 
    }
 }
 

-

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

-\subsection{Propositional 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{...and its limitations}
+\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
 
 
 eta law
 


@@ -995,11 +1161,158 @@ congruence
 
 UIP
 
 
 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}
 
 \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}
 \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.
+

 
 

-\subsection{Univalence foundations}

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


@@ -1025,6 +1338,145 @@ UIP
 \section{\mykant}
 \label{sec:kant}
 
 \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
 
 
 \appendix
 


@@ -1035,7 +1487,7 @@ the type of relation being established and the syntactic elements appearing,
 for example
 
 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
 for example
 
 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{

-  Typing derivations here.
+  \centering{Typing derivations here.}

 }
 
 In the languages presented and Agda code samples I also highlight the syntax,
 }
 
 In the languages presented and Agda code samples I also highlight the syntax,


@@ -1114,6 +1566,19 @@ module ITT where
     (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))
     (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{*}
 \end{code}
 
 \nocite{*}