From: Francesco Mazzoli <f@mazzo.li>
Date: Fri, 7 Jun 2013 14:32:55 +0000 (+0100)
Subject: ...
X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=2a33412a41393afc6574354625c0d9434f099754

...
---

diff --git a/thesis.lagda b/thesis.lagda
index 794b10d..97e846f 100644
--- a/thesis.lagda
+++ b/thesis.lagda
@@ -62,11 +62,11 @@
 
 \newcommand{\mysyn}{\AgdaKeyword}
 \newcommand{\mytyc}{\AgdaDatatype}
+% TODO have this with math mode so I can have subscripts
 \newcommand{\mydc}{\AgdaInductiveConstructor}
 \newcommand{\myfld}{\AgdaField}
 \newcommand{\myfun}{\AgdaFunction}
-% TODO make this use AgdaBound
-\newcommand{\myb}[1]{\AgdaBound{#1}}
+\newcommand{\myb}[1]{\AgdaBound{$#1$}}
 \newcommand{\myfield}{\AgdaField}
 \newcommand{\myind}{\AgdaIndent}
 \newcommand{\mykant}{\textsc{Kant}}
@@ -74,7 +74,6 @@
 \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}
@@ -92,7 +91,9 @@
         \framebox[\textwidth]{
           \parbox{\textwidth}{
             \vspace{0.1cm}
-            #3
+            \centering{
+              #3
+            }
             \vspace{0.1cm}
           }
         }
@@ -138,7 +139,7 @@
 \newcommand{\myempty}{\mytyc{Empty}}
 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
-\newcommand{\myarg}{\_}
+\newcommand{\myarg}{-}
 \newcommand{\myderivsp}{\vspace{0.3cm}}
 \newcommand{\mytyp}{\mytyc{Type}}
 \newcommand{\myneg}{\myfun{$\neg$}}
@@ -168,16 +169,18 @@
 \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{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
+\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
-\newcommand{\mybot}{\bot}
-\newcommand{\mytop}{\top}
+\newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
+\newcommand{\mybot}{\mytyc{$\bot$}}
+\newcommand{\mytop}{\mytyc{$\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{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
+\newcommand{\myeq}{\mathrel{\mytyc{=}}}
 \newcommand{\myprop}{\mytyc{Prop}}
 \newcommand{\mytmup}{\mytmsyn\uparrow}
 \newcommand{\mydefs}{\Delta}
@@ -190,8 +193,8 @@
 \newcommand{\mydeclsyn}{\myse{decl}}
 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
 \newcommand{\mypost}[2]{\mysyn{postulate}\ #1 : #2}
-\newcommand{\myadt}[4]{\mysyn{data}\ #1 : #2 \myarr \mytyp\ \mysyn{where}\ #3\{ #4 \}}
-\newcommand{\myreco}[4]{\mysyn{record}\ #1 : #2 \myarr \mytyp\ \mysyn{where}\ #3\ \{ #4 \}}
+\newcommand{\myadt}[4]{\mysyn{data}\ #1 : #2\ \mysyn{where}\ #3\{ #4 \}}
+\newcommand{\myreco}[4]{\mysyn{record}\ #1 : #2\ \mysyn{where}\ #3\ \{ #4 \}}
 % TODO change vdash
 \newcommand{\myelabt}{\vdash}
 \newcommand{\myelabf}{\rhd}
@@ -209,6 +212,7 @@
 % \newcommand{\mytesctx}{\
 \newcommand{\mytelesyn}{\myse{telescope}}
 \newcommand{\myrecs}{\mymeta{recs}}
+\newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
 
 %% -----------------------------------------------------------------------------
 
@@ -341,12 +345,12 @@ 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.
+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.  Reduction is unchanged from the untyped
+$\lambda$-calculus.
 
 \begin{figure}[t]
   \mydesc{syntax}{ }{
@@ -362,7 +366,6 @@ unchanged from the untyped $\lambda$-calculus.
   }
   
   \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
-    \centering{
       \begin{tabular}{ccc}
         \AxiomC{$\myctx(x) = A$}
         \UnaryInfC{$\myjud{\myb{x}}{A}$}
@@ -377,7 +380,6 @@ unchanged from the untyped $\lambda$-calculus.
         \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.}
@@ -419,18 +421,14 @@ adding a combinator that recurses:
 \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
@@ -471,7 +469,6 @@ shown in figure \ref{fig:natded}.
 }
 
 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
-  \centering{
     \begin{tabular}{cc}
       $
       \begin{array}{l@{ }l@{\ }c@{\ }l}
@@ -489,11 +486,9 @@ shown in figure \ref{fig:natded}.
       \end{array}
       $
     \end{tabular}
-  }
 }
 
 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
-  \centering{
     \begin{tabular}{cc}
       \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
       \UnaryInfC{$\myjud{\mytt}{\myunit}$}
@@ -503,9 +498,9 @@ shown in figure \ref{fig:natded}.
       \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}$}
@@ -516,9 +511,9 @@ shown in figure \ref{fig:natded}.
       \DisplayProof
 
     \end{tabular}
-  }
+
   \myderivsp
-  \centering{
+
     \begin{tabular}{cc}
       \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
       \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
@@ -526,9 +521,9 @@ shown in figure \ref{fig:natded}.
       \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
       \DisplayProof
     \end{tabular}
-  }
+
   \myderivsp
-  \centering{
+
     \begin{tabular}{ccc}
       \AxiomC{$\myjud{\mytmm}{\mytya}$}
       \AxiomC{$\myjud{\mytmn}{\mytyb}$}
@@ -543,29 +538,27 @@ shown in figure \ref{fig:natded}.
       \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.
+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{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
+$\mypair{\myarg}{\myarg}$ 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.
+}$), corresponding to the logical \emph{ex falso quodlibet}.
 
 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
@@ -594,6 +587,7 @@ including bottom:
 \]
 
 \subsection{Inductive data}
+\label{sec:ind-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
@@ -617,7 +611,6 @@ lists will be the usual folding operation ($\myfoldr$).  See figure
   $
 }
 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
-  \centering{
   $
   \begin{array}{l@{\ }c@{\ }l}
     \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
@@ -627,9 +620,7 @@ lists will be the usual folding operation ($\myfoldr$).  See figure
   \end{array}
   $
 }
-}
 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
-  \centering{
     \begin{tabular}{cc}
       \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
       \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
@@ -640,15 +631,13 @@ lists will be the usual folding operation ($\myfoldr$).  See figure
       \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}
@@ -746,12 +735,13 @@ 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}.
+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 and all the examples is reproduced in appendix
+\ref{app:agda-itt}.
 
 \begin{figure}[t]
 \mydesc{syntax}{ }{
@@ -778,8 +768,7 @@ reproduced in appendix \ref{app:agda-code}.
 }
 
 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
-  \centering{
-    \begin{tabular}{cc}
+    \begin{tabular}{ccc}
       $
       \begin{array}{l@{ }l@{\ }c@{\ }l}
         \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
@@ -790,14 +779,15 @@ reproduced in appendix \ref{app:agda-code}.
       $
       \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}
     $
+    \end{tabular}
+
     \myderivsp
 
     $
@@ -806,7 +796,6 @@ reproduced in appendix \ref{app:agda-code}.
       \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}
@@ -816,7 +805,6 @@ reproduced in appendix \ref{app:agda-code}.
 \label{sec:term-types}
 
 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
-  \centering{
     \begin{tabular}{cc}
       \AxiomC{$\myjud{\mytmt}{\mytya}$}
       \AxiomC{$\mytya \mydefeq \mytyb$}
@@ -827,7 +815,6 @@ reproduced in appendix \ref{app:agda-code}.
       \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
@@ -867,7 +854,6 @@ can be employed to lift the burden of explicitly handling universes.
 
 \begin{minipage}{0.5\textwidth}
   \mydesc{context validity:}{\myvalid{\myctx}}{
-    \centering{
       \begin{tabular}{cc}
         \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
         \UnaryInfC{$\myvalid{\myemptyctx}$}
@@ -877,16 +863,13 @@ can be employed to lift the burden of explicitly handling universes.
         \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}
@@ -902,7 +885,6 @@ context.
 \subsubsection{$\myunit$, $\myempty$}
 
 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
-  \centering{
     \begin{tabular}{ccc}
       \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
       \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
@@ -923,7 +905,6 @@ context.
       \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
       \DisplayProof
     \end{tabular}
-  }
 }
 
 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
@@ -933,7 +914,6 @@ 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}$}
@@ -955,8 +935,6 @@ sure that we are invoking $\myabsurd{}$ over a type.
     \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
@@ -980,7 +958,6 @@ 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}}$}
@@ -998,29 +975,48 @@ the updated knowledge on the value of $\myb{x}$.
       \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.
+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.
+Following this intuition, in the introduction rule, the return type is
+typechecked in a context with an abstracted variable of lhs' type, and
+in the elimination rule the actual argument is substituted in the return
+type.  Keeping the correspondence with logic alive, dependent functions
+are much like universal quantifiers ($\forall$) in logic.
+
+For example, assuming that we have lists and natural numbers in our
+language, using dependent functions we would be able to
+write:
+\[
+\begin{array}{c@{\ }c@{\ }l@{\ }}
+\myfun{length} & : & (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
+\myarg \myfun{$>$} \myarg & : & \mynat \myarr \mynat \myarr \mytyp_0 \\
+\myfun{head} & : & (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
+               \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{>}} 0 \myarr
+               \myb{A}
+\end{array}
+\]
+
+\myfun{length} is the usual polymorphic length function. $\myfun{>}$ is
+a function that takes two naturals and returns a type: if the lhs is
+greater then the rhs, $\myunit$ is returned, $\myempty$ otherwise.  This
+way, we can express a `non-emptyness' condition in $\myfun{head}$, by
+including a proof that the length of the list argument is non-zero.
+This allows us to rule out the `empty list' case, so that we can safely
+return the first element.
 
 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}}$}
@@ -1042,16 +1038,24 @@ type-level binders, $\myprod$ and $\mytyc{W}$.
       \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
       \DisplayProof
     \end{tabular}
-
-  }
 }
 
+If dependent functions are a generalisation of $\myarr$ in the STLC,
+dependent products are a generalisation of $\myprod$ in the STLC.  The
+improvement is that the second element's type can depend on the value of
+the first element.  The corrispondence with logic is through the
+existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
+expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
+The first element will be a number, and the second evidence that the
+number is even.  This highlights the fact that we are working in a
+constructive logic: if we have an existence proof, we can always ask for
+a witness.  This means, for instance, that $\neg \forall \neg$ is not
+equivalent to $\exists$.
 
 \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}}$}
@@ -1074,18 +1078,19 @@ type-level binders, $\myprod$ and $\mytyc{W}$.
      }$}
      \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.
+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.  As in the previous section, everything presented is
+formalised in Agda in appendix \ref{app:agda-code}.
 
 \subsection{Propositional equality}
 
@@ -1104,17 +1109,14 @@ not have a fully satisfactory solution, yet.
 \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}$}
@@ -1126,17 +1128,16 @@ not have a fully satisfactory solution, yet.
     \begin{tabular}{cc}
       \AxiomC{\phantom{$\myctx P \mytyp_l$}}
       \noLine
-      \UnaryInfC{$\myjud{\mytmt}{\mytya}$}
-      \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\mytmt \mypeq{\mytya} \mytmt}$}
+      \UnaryInfC{$\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn$}
+      \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
       \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{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\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
@@ -1224,9 +1225,10 @@ no term of type
 \]
 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
+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 extensionally equal, and we can in fact
+prove that
 \[
 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
 \]
@@ -1250,11 +1252,9 @@ 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
@@ -1284,13 +1284,13 @@ 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}}}$}
+  \AxiomC{$\hspace{1.1cm}\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\hspace{1.1cm}$}
   \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}}$}
+  \UnaryInfC{$\hspace{1.4cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.4cm}$}
   \RightLabel{$\myrefl$}
   \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
 \end{prooftree}
@@ -1313,23 +1313,149 @@ equal; and providing a value-level equality based on similar principles.  A
 brief overview is given below,
 
 \mydesc{syntax}{ }{
+    $\mytyp_l$ is replaced by $\mytyp$. \\
+    $
+    \begin{array}{r@{\ }c@{\ }l}
+      \mytmsyn & ::= & \cdots \\
+      &  |  & \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 \myeq \mytmsyn \mysynsep
+      \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+    \end{array}
+    $
+}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+
+  There is only $\mytyp$, which corresponds to $\mytyp_0$.  \\ Thus all
+  the type-formers take $\mytyp$ arguments and form a $\mytyp$. \\ \ \\
+
+  % TODO insert large eliminator
+
+  \begin{tabular}{cc}
+    \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+    \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
+    \DisplayProof
+    &
+    \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+    \AxiomC{$\myjud{\mytmt}{\mytya}$}
+    \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
+    \DisplayProof
+  \end{tabular}
+
+  \myderivsp
+
+  \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+  \AxiomC{$\myjud{\mytmt}{\mytya}$}
+  \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
+  \DisplayProof
+}
+
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+    \begin{tabular}{cc}
+      \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
+      \UnaryInfC{$\myjud{\mytop}{\myprop}$}
+      \noLine
+      \UnaryInfC{$\myjud{\mybot}{\myprop}$}
+      \DisplayProof
+      &
+      \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+      \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
+      \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
+      \noLine
+      \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
+      \DisplayProof
+    \end{tabular}
+
+    \myderivsp
+
+    \begin{tabular}{cc}
+      \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+      \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
+      \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
+      \DisplayProof
+      &
+      \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+      \AxiomC{$\myjud{\myse{B}}{\mytyp}$}
+      \BinaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
+      \DisplayProof
+    \end{tabular}
+
+    \myderivsp
+
+    \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+    \AxiomC{$\myjud{\mytmm}{\myse{A}}$}
+    \AxiomC{$\myjud{\myse{B}}{\mytyp}$}
+    \AxiomC{$\myjud{\mytmn}{\myse{B}}$}
+    \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
+    \DisplayProof
+}
+
+\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
+    \begin{tabular}{cc}
+    $
+    \begin{array}{l@{\ }c@{\ }l}
+      \myprdec{\mybot} & \myred & \myempty \\
+      \myprdec{\mytop} & \myred & \myunit
+    \end{array}
+    $
+    &
+    $
+    \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
+      \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
+      \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
+             \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
+    \end{array}
+    $
+    \end{tabular}
+}
+
+\mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
+    $
+      \begin{array}{c@{\ }c@{\ }c@{\ }l}
+        \myempty & \myeq & \myempty & \myred \mytop \\
+        \myunit  & \myeq &  \myunit & \myred  \mytop \\
+        \mybool  & \myeq &  \mybool &   \myred  \mytop \\
+        \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \\
+        \multicolumn{4}{l}{
+          \myind{2} \mytya_1 \myeq \mytyb_1 \myand 
+                  \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1 \myeq \mytyb_2}
+                  } \\
+      \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
+      \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
+      \mytya & \myeq & \mytyb & \myred \mybot\ \text{for other canonical types.}
+      \end{array}
+    $
+}
+
+\mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
   $
-  \begin{array}{r@{\ }c@{\ }l}
-    \mytmsyn & ::= & \cdots \\
-             &  |  & \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}
+  \begin{array}{l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
+    \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
+    \mycoe & \myunit  & \myunit  & \myse{Q} & \mytt & \myred & \mytt \\
+    \mycoe & \mybool  & \mybool  & \myse{Q} & \mytrue & \myred & \mytrue \\
+    \mycoe & \mybool  & \mybool  & \myse{Q} & \myfalse & \myred & \myfalse \\
+    \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
+             (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
+             \mytmt_1 & \myred &
+           foo \\
+    \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
+             (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
+             \mytmt_1 & \myred &
+           \cdots \\
+
+    \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
+             (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
+             \mytmt_1 & \myred &
+           \cdots \\
+
+    \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}
   \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
@@ -1487,7 +1613,6 @@ sure not to have duplicate top names, so we enforce that.
 %                        \mysynsep \mytyc{D}.\myfun{f} \mysynsep 
 
 \mydesc{context validity:}{\myvalid{\myctx}}{
-  \centering{
     \begin{tabular}{ccc}
       \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
       \UnaryInfC{$\myvalid{\myemptyctx}$}
@@ -1503,7 +1628,6 @@ sure not to have duplicate top names, so we enforce that.
       \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
       \DisplayProof
     \end{tabular}
-  }
 }
 
 Now we can present the reduction rules, which are unsurprising.  We have the
@@ -1513,7 +1637,6 @@ discard type annotations.  For this reason the new reduction rules are
 dependent on the context:
 
 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
-  \centering{
     \begin{tabular}{ccc}
       \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
       \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
@@ -1528,7 +1651,6 @@ dependent on the context:
       \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
       \DisplayProof
     \end{tabular}
-  }
 }
 
 We want to define a \emph{weak head normal form} (WHNF) for our terms, to give
@@ -1541,8 +1663,7 @@ $\mytmm \mynf \mytmn$ to indicate that $\mytmm$'s normal form is $\mytmn$.
 This way, we can avoid the non syntax-directed conversion rule, giving a more
 algorithmic presentation of type checking.
 
-\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytysyn}{   
-  \centering{
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{   
     \begin{tabular}{ccc}
       \AxiomC{$\myb{x} : A \in \myctx$ or $\myb{x} \mapsto \mytmt : A \in \myctx$}
       \UnaryInfC{$\myinf{\myb{x}}{A}$}
@@ -1566,7 +1687,6 @@ algorithmic presentation of type checking.
     \AxiomC{$\mychkk{\myctx; \myb{x}: \mytyb}{\mytmt}{\myse{C}}$}
     \BinaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\mytya}$}
     \DisplayProof
-  }
 }
 
 \subsection{Elaboration}
@@ -1584,10 +1704,16 @@ algorithmic presentation of type checking.
   $
 }
 
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{   
+
+}
+
 \subsubsection{Values and postulated variables}
 
+As mentioned, in \mykant\ we can defined top level variables, with or without
+a body.  We call the variables
+
 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
-  \centering{
     \begin{tabular}{cc}
       \AxiomC{$\myjud{\mytmt}{\mytya}$}
       \AxiomC{$\myfun{f} \not\in \myctx$}
@@ -1607,7 +1733,6 @@ algorithmic presentation of type checking.
       \DisplayProof
     \end{tabular}
 }
-}
 
 \subsubsection{User defined types}
 
@@ -1619,15 +1744,32 @@ algorithmic presentation of type checking.
   $
 }
 
+\mydesc{typing:}{ }{
+    \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+    \AxiomC{$\mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
+      \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
+    \BinaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
+    \DisplayProof
+    % TODO
+
+    \myderivsp
+
+    \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+    \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \myarr
+      \myapp{\mytyc{D}}{\mytelee} \myarr \myse{F}$}
+    \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
+    \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{TODO}$}
+    \DisplayProof
+}
+
 \subsubsection{Data types}
 
 \begin{figure}[t]
-  \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
-    \centering{
+  \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
       $
-      \begin{array}{r@{\ }c@{\ }l}
-        \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
-        & \myelabf &
+      \begin{array}{r@{\ }l}
+         & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
+        \myelabf &
         
         \begin{array}{r@{\ }c@{\ }l}
           \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\myvec{\mytmsyn}} \mysynsep
@@ -1635,11 +1777,9 @@ algorithmic presentation of type checking.
         \end{array}
       \end{array}
       $
-    }
   }
 
   \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
-    \centering{
       \AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
       \AxiomC{$\mytyc{D} \not\in \myctx$}
       \noLine
@@ -1675,11 +1815,9 @@ algorithmic presentation of type checking.
         \end{array}
         $}
       \DisplayProof
-    }
   }
 
-  \mydesc{reduction elaboration:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{  
-    \centering{
+  \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{  
       \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
       \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
       \BinaryInfC{$
@@ -1687,13 +1825,12 @@ algorithmic presentation of type checking.
           \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)} \\ \\
         \begin{array}{@{}l l@{\ } l@{} r c l}
           \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
-                         & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{t}}); \mytele & ) & \mymetagoes &  (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
+                         & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes &  (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
                          & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
           \end{array}
         \end{array}
         $}
       \DisplayProof
-    }
   }
 
   \caption{Elaborations for data types.}
@@ -1705,7 +1842,6 @@ algorithmic presentation of type checking.
 
 \begin{figure}[t]
 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
-  \centering{
     $
     \begin{array}{r@{\ }c@{\ }l}
       \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
@@ -1717,12 +1853,10 @@ algorithmic presentation of type checking.
              \end{array}
     \end{array}
     $
-  }
 }
 
 
 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
-  \centering{
     \AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
     \AxiomC{$\mytyc{D} \not\in \myctx$}
     \noLine
@@ -1737,15 +1871,12 @@ algorithmic presentation of type checking.
       \end{array}
       $}
     \DisplayProof
-  }
 }
 
-  \mydesc{reduction elaboration:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
-    \centering{
+  \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
       \AxiomC{$\mytyc{D} \in \myctx$}
       \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
       \DisplayProof
-    }
   }
 
   \caption{Elaborations for records.}
@@ -1756,12 +1887,17 @@ algorithmic presentation of type checking.
 \subsection{Type hierarchy}
 \label{sec:term-hierarchy}
 
-\subsection{Defined and postulated variables}
+\subsection{Observational equality, \mykant\ style}
 
-As mentioned, in \mykant\ we can defined top level variables, with or without
-a body.  We call the variables
-
-\subsection{Observational equality}
+\mydesc{syntax}{ }{
+  $
+  \begin{array}{r@{\ }c@{\ }l}
+    \mytmsyn & ::= & \mytmsyn \myeq \mytmsyn \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+             &  |  & \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+                     \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+  \end{array}
+  $
+}
 
 \section{\mykant : The practice}
 \label{sec:kant-practice}
@@ -1886,7 +2022,7 @@ the type of relation being established and the syntactic elements appearing,
 for example
 
 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
-  \centering{Typing derivations here.}
+  Typing derivations here.
 }
 
 In the languages presented and Agda code samples I also highlight the syntax,
@@ -1925,19 +2061,27 @@ conclusions, each on a separate line:
   \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
 \end{prooftree}
 
-\section{Agda rendition of core ITT}
-\label{app:agda-code}
+\section{Agda rendition of ITT}
+\label{app:agda-itt}
+
+Note that in what follows rules for `base' types are
+universe-polymorphic, to reflect the exposition.  Derived definitions,
+on the other hand, mostly work with \mytyc{Set}, reflecting the fact
+that in the theory presented we don't have universe polymorphism.
 
 \begin{code}
 module ITT where
   open import Level
 
-  data ⊥ : Set where
+  data Empty : Set where
 
-  absurd : ∀ {a} {A : Set a} → ⊥ → A
+  absurd : ∀ {a} {A : Set a} → Empty → A
   absurd ()
 
-  record ⊤ : Set where
+  ¬_ : ∀ {a} → (A : Set a) → Set a
+  ¬ A = A → Empty
+
+  record Unit : Set where
     constructor tt
 
   record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
@@ -1966,6 +2110,56 @@ module ITT where
     C x                       -- ...C always holds.
   rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
 
+module Examples-→ where
+  open ITT
+
+  data ℕ : Set where
+    zero : ℕ
+    suc : ℕ → ℕ
+
+  -- These pragmas are needed so we can use number literals.
+  {-# BUILTIN NATURAL ℕ #-}
+  {-# BUILTIN ZERO zero #-}
+  {-# BUILTIN SUC suc #-}
+
+  data List (A : Set) : Set where
+    [] : List A
+    _∷_ : A → List A → List A
+
+  length : ∀ {A} → List A → ℕ
+  length [] = zero
+  length (_ ∷ l) = suc (length l)
+
+  _>_ : ℕ → ℕ → Set
+  zero > _ = Empty
+  suc _ > zero = Unit
+  suc x > suc y = x > y
+
+  head : ∀ {A} → (l : List A) → length l > 0 → A
+  head [] p = absurd p
+  head (x ∷ _) _ = x
+
+module Examples-× where
+  open ITT
+  open Examples-→
+
+  even : ℕ → Set
+  even zero = Unit
+  even (suc zero) = Empty
+  even (suc (suc n)) = even n
+
+  6-is-even : even 6
+  6-is-even = tt
+
+  5-is-not-even : ¬ (even 5)
+  5-is-not-even = absurd
+  
+  there-is-an-even-number : ℕ × even
+  there-is-an-even-number = 6 , 6-is-even
+
+module Equality where
+  open ITT
+  
   data _≡_ {a} {A : Set a} : A → A → Set a where
     refl : ∀ x → x ≡ x
 
@@ -1974,10 +2168,17 @@ module ITT where
     ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
   ≡-elim 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 : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
   subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
+
+  sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
+  sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
+
+  trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
+  trans x y z p q = subst (λ z′ → x ≡ z′) q p
+
+  cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y 
+  cong x y p f = subst (λ y′ → f x ≡ f y′) p (refl (f x))
 \end{code}
 
 \nocite{*}