+ \centering{
+ \begin{tabular}{cc}
+ $
+ \begin{array}{l@{ }l@{\ }c@{\ }l}
+ \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
+ \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
+ \end{array}
+ $
+ &
+ $
+ \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}
+ $
+ \myderivsp
+
+ $
+ \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
+ \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
+ \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}
+\end{figure}
+
+\subsubsection{Types are terms, some terms are types}
+\label{sec:term-types}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\mytya \mydefeq \mytyb$}
+ \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
+ \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
+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
+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.
+
+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
+`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}
+
+\begin{minipage}{0.5\textwidth}
+ \mydesc{context validity:}{\myvalid{\myctx}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myvalid{\myemptyctx}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \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}
+
+We need to refine the notion context to make sure that every variable appearing
+is typed correctly, or that in other words each type appearing in the context is
+indeed a type and not a value. In every other rule, if no premises are present,
+we assume the context in the conclusion to be valid.
+
+Then we can re-introduce the old rule to get the type of a variable for a
+context.
+
+\subsubsection{$\myunit$, $\myempty$}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myjud{\mytt}{\myunit}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\myempty}$}
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
+with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
+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}$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
+ \DisplayProof
+ \end{tabular}
+ \myderivsp
+
+ \AxiomC{$\myjud{\mytmt}{\mybool}$}
+ \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
+ \noLine
+ \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
+
+ }
+}