+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}