+\end{equation*}
+Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
+3 dimensions:
+\begin{description}
+\item[Terms depending on types (towards $\lambda{2}$)] In other words, we can
+ quantify over types in our type signatures: $(\lambda A : \lctype. \lambda x :
+ A. x) : \forall A. A \to A$. The first and most famous instance of this idea
+ has been System F. This gives us a form of polymorphism and has been wildly
+ successful, also thanks to a well known inference algorithm for a restricted
+ version of System F known as Hindley-Milner. Languages like Haskell and SML
+ are based on this discipline.
+\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other
+ words, we have type operators: $(\lambda A : \lctype. \lambda R : \lctype. (A \to R) \to R) : \lctype \to \lctype \to \lctype$.
+\item[Types depending on terms (towards $\lambda{P}$)] Also known as ``dependent
+ types'', give great expressive power: $(\lambda x :
+ \lcbool. \lcite{x}{\mathbb{N}}{\mathbb{Q}}) : \lcbool \to \lctype$.
+\end{description}
+
+All the systems preserve the properties that make the STLC well behaved (some of
+which I haven't mentioned yet). The system we are going to focus on,
+Intuitionistic Type Theory, has all of the above additions, and thus would sit
+where $\lambda{C}$ sits in the ``$\lambda$-cube'' above.
+
+\section{Intuitionistic Type Theory}
+
+In this section I will describe