1 files changed, 313 insertions, 89 deletions
diff --git a/docs/background.tex b/docs/background.tex
index 507dbf8..ff4e8cd 100644
--- a/docs/background.tex
+++ b/docs/background.tex
@@ -82,6 +82,8 @@
 
 \maketitle
 
+\setlength{\tabcolsep}{12pt}
+
 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.
@@ -110,41 +112,50 @@ 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}{\ |\ }
+\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$}}
 
+\begin{center}
+\axname{syntax}
 \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\}
+  \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{eqnarray*}
+\end{center}
+
 
 % 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:
 
-\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$.
+occurrences of $x$ with $\termm$ in $\termt$.  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.
 
 % % TODO put the trans closure
 
@@ -161,9 +172,9 @@ material analysed.
 
 \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.
@@ -174,53 +185,63 @@ reads ``in context $\Gamma$, term $\termt$ has type $\tya$''.
 The syntax for types is as follows:
 
 \newcommand{\tyarr}{\to}
+\newcommand{\tysyn}{\mathit{type}}
+\newcommand{\ctxsyn}{\mathit{context}}
+\newcommand{\emptyctx}{\cdot}
 
-\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.
+$\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}
+  \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
+
+  \vspace{0.5cm}
+
+  \begin{tabular}{c c c}
     \AxiomC{}
-    \UnaryInfC{$\Gamma, x : \tya \vdash x : \tya$}
-  \end{prooftree}
-  \begin{prooftree}
-    \AxiomC{$\Gamma, x : \tya \vdash \termt : \tyb$}
+    \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),
 and enjoys a number of properties.  Two of them are expected in most type
 systems: %TODO add credit to pierce
 \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}
@@ -232,34 +253,37 @@ give types to the non-normalising term shown before:
   \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
 \end{equation*}
 
-\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1. #2}
+\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #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]
+  \termsyn ::= \dots \separ  \lcfix{x : \tysyn}{\termsyn}
 \end{equation*}
 \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}
+\begin{equation*}
+  \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x]
+\end{equation*}
 
 However, we will keep STLC without such a facility. In the next section we shall
 see why that is preferable for our needs.
 
 \subsection{The Curry-Howard correspondence}
+\label{sec:curry-howard}
+
+\newcommand{\lcunit}{\mathsf{()}}
 
 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.
+is known as the Curry-Howard correspondence, or isomorphism.
 
 The ``arrow'' ($\to$) type corresponds to implication.  If we wished to
-prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tyc
+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*}
@@ -268,9 +292,10 @@ correct type:
 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.
+(or products) 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.
+Conversely, $\top$ is the type with just one trivial element, $\lcunit$.
 
 \newcommand{\lcinl}{\mathsf{inl}\appspace}
 \newcommand{\lcinr}{\mathsf{inr}\appspace}
@@ -286,21 +311,18 @@ presented, then we can derive any type, which expresses absurdity.
 \newcommand{\botel}{\bot E}
 \newcommand{\lcabsurd}{\mathsf{absurd}\appspace}
 
-\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{eqnarray*}
+    \termsyn & ::= & \dots \\
+             &  |  & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
+             &  |  & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
+             &  |  & \lcunit \\
+    \tysyn & ::= & \dots \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
+  \end{eqnarray*}
+\end{center}
+\begin{center}
+  \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
   \begin{prooftree}
     \AxiomC{$\Gamma \vdash \termt : \tya$}
     \RightLabel{$\orint$}
@@ -315,43 +337,74 @@ presented, then we can derive any type, which expresses absurdity.
     \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}
+    \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 we will not touch those subjects.}.
+
+Finally, going back to our $\mathsf{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{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
+\newcommand{\lcforall}[3]{\forall #1 : #2 \absspace.\absspace #3}
+\newcommand{\lcexists}[3]{\exists #1 : #2 \absspace.\absspace #3}
 
 The STLC can be made more expressive in various ways.  Henk Barendregt
 succinctly expressed geometrically how we can expand our type system:
@@ -375,17 +428,15 @@ 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
+  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$.
+  words, 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: $(\lambda x :
-  \lcbool. \lcite{x}{\mathbb{N}}{\mathbb{Q}}) : \lcbool \to \lctype$.
+  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 (some of
@@ -395,6 +446,179 @@ where $\lambda{C}$ sits in the ``$\lambda$-cube'' above.
 
 \section{Intuitionistic Type Theory}
 
-In this section I will describe 
+Intuitionistic Type Theory (ITT) is a very expressive system first described by
+Per Martin-L\"{o}f at the end of the 70s.  It extends the STLC giving it all the
+properties described above, while retaining good computational properties.  Here
+we will present a core type theory and illustrate its components and properties
+one by one, and then describe the various additions that make it useful as a
+programming language and as a theorem prover.
+
+\newcommand{\lcset}[1]{\mathsf{Type}_{#1}}
+\newcommand{\lcsetz}{\mathsf{Type}}
+\newcommand{\defeq}{\equiv}
+
+\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) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
+         &  |  & \bot \separ \lcabsurd \termt \\
+         &  |  & \lcset{n} \\
+   n     & \in & \mathbb{N}
+ \end{eqnarray*}
+
+  \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+  \vspace{0.5cm}
+
+  \begin{tabular}{c c c}
+    \AxiomC{}
+    \RightLabel{var}
+    \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
+    \DisplayProof
+    &
+    \AxiomC{$\Gamma \vdash \termt : \bot$}
+    \RightLabel{$\bot E$}
+    \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : A$}
+    \DisplayProof
+    &
+    \AxiomC{$\Gamma \vdash \termt : \tya$}
+    \AxiomC{$\tya \defeq \tyb$}
+    \RightLabel{$\defeq$ type}
+    \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
+    \DisplayProof
+  \end{tabular}
+
+  \vspace{0.5cm}
+
+  \begin{tabular}{c c}
+    \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
+    \RightLabel{$\forall I$}
+    \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$}
+    \RightLabel{$\forall E$}
+    \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm / x]$}
+    \DisplayProof
+  \end{tabular}
+
+  \vspace{0.5cm}
+
+  \begin{tabular}{c c}
+    \AxiomC{$\Gamma \vdash \termt : \tya$}
+    \AxiomC{$\Gamma \vdash \termm : \tyb[\termt / x]$}
+    \RightLabel{$\exists I$}
+    \BinaryInfC{$\Gamma \vdash (\termt, \termm) : \lcexists{x}{\tya}{\tyb}$}
+    \DisplayProof
+    &
+    \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
+    \RightLabel{$\exists E_{1,2}$}
+    \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
+    \noLine
+    \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt / x]$}
+    \DisplayProof
+  \end{tabular}
+
+  \vspace{0.5cm}
+
+  \begin{tabular}{c c}
+    \AxiomC{}
+    \RightLabel{type}
+    \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
+    \DisplayProof
+    &
+    \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
+    \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
+    \RightLabel{$\forall, \exists$ type}
+    \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 / x] \\
+    \lcfst (\termt, \termm) & \bred & \termt \\
+    \lcsnd (\termt, \termm) & \bred & \termm
+  \end{eqnarray*}
+\end{center}
+
+I will abbreviate $\lcset{0}$ as $\lcsetz$.
+
+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 terms and types are kept well separated (terms never go
+``right of the colon''), in ITT types can freely depend on terms.
+
+This relation is expressed in the typing rules for $\forall$ and $\exists$: 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 the next
+section.
+
+$\forall$ and $\exists$ are at the core of the machinery of ITT:
+
+\begin{description}
+\item[$\forall$] is a generalisation of $\tyarr$ in the STLC and expresses
+  universal quantification in our logic.  In the literature this is also known
+  as ``dependent product'' and shown as $\Pi$, following an interpretation of
+  functions as infinitary products. We will just call it ``dependent function'',
+  reserving ``product'' for $\exists$.
+
+\item[$\exists$] is a generalisation of $\wedge$ in the extended STLC of section
+  \ref{sec:curry-howard}, and thus we will call it ``dependent product''.  In
+  our logic, it represents existential quantification.
+
+  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 $\vee$, where the first element
+  of the pair is the ``tag'' that decides which type the second element will
+  have.
+\end{description}
+
+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 $\defeq$ as
+the smallest 
+
+\begin{thebibliography}{9}
+
+\bibitem{levitation}
+  James Chapman, Pierre-Evariste Dagand, Conor McBride, and Peter Morris.
+  \emph{The gentle art of levitation}.
+  SIGPLAN Not., 45:3–14, September 2010.
+
+\bibitem{outsidein}
+  Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin
+  Sulzmann.
+  \emph{OutsideIn(X): Modular Type inference with local assumptions}.
+  Journal of Functional Programming, 21, 2011.
+
+\bibitem{haskell-promotion}
+  Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
+  Dimitrios Vytiniotis, and Jos\'{e} Pedro Magalh\~{a}es.
+  \emph{Giving Haskell a promotion}.
+  In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and
+  Implementation, TLDI ’12, pages 53–66, New York, NY, USA, 2012. ACM. doi:
+  10.1145/2103786.2103795.
+
+\bibitem{idris}
+  Edwin Brady.
+  \emph{Implementing General Purpose Dependently Typed Programming Languages}.
+  Unpublished draft.
+
+\bibitem{bidirectional}
+  Benjamin C. Pierce and David N. Turner.
+  \emph{Local type inference}.
+  ACM Transactions on Programming Languages and Systems, 22(1):1–44, January
+  2000. ISSN 0164-0925. doi: 10.1145/345099.345100.
+
+\end{thebibliography}
 
 \end{document}