Homotopy Type Theory homotopy type theory > history (Rev #9)

…

\tableofcontents

\section{Idea}

Homotopy type theory is a framework of dependent type theories which additionally consists of

• identity types

• dependent product types?

• dependent sum types?

• univalent universes

• inductive types?, higher inductive types, inductive type families?, et cetera.

\section{Presentation}

The model of homotopy type theory we shall be presenting here is the objective type theory version of homotopy type theory. There are multiple reasons for this:

• Since objective type theory lacks definitional equality,

  • The ruleset is simpler in the objective type theory model of homotopy type theory than other models such as Martin-Löf type theory, cubical type theory, or higher observational type theory

  • The results in objective type theory are more general than in models which use definitional equality

  • It is similar to other non-type theory foundations such as the various flavors of set theory, since it also only has one notion of equality, which is propositional equality in both objective type theory and set theory, and uses propositional equality to define terms and types.

• From a more practical standpoint, objective type theory not only has decidable type checking, it has polynomial (quadratic) time type checking, which makes it efficient from a computational standpoint.

\subsection{Types and terms}

As with any type theory, the basic judgments of this model are judging $A$ to be a type, $A \; \mathrm{type}$, and judging $a$ to be a term of $A$, $a:A$, and judging $\Gamma$ to be a context, $\Gamma \; \mathrm{ctx}$. Contexts are lists of type and term judgments.

\subsection{Dependent types and sections}

A dependent type is a type $B$ in the context of the variable judgment $x:A$, $x:A \vdash B \; \mathrm{type}$. The dependent type is usually written as $B(x)$ to indicate the dependence upon $x$.

A section is a term $b:B$ in the context of the variable judgment $x:A$, $x:A \vdash b:B$. Similarly for the case for dependent types, sections are usually written as $b(x)$ to indicate its dependence upon $x$.

\subsection{Variable, Substitution, and Weakening rules}

…

\subsection{Russell universes}

Universes are the types of types in type theory.

We introduce a universe $U$, with rules for universe formation and type reflection

\subsection{Equality}

Equality in type theory is represented by the identity type, which is also called the path type or identification type. The terms of the identity type could be called paths or identifications.

…

\subsection{Definitions}

\subsection{Functions}

\subsection{Dependent products}

\subsection{Products}

\subsection{Dependent sums}

\subsection{Sums}

\subsection{Empty type}

\subsection{Unit type}

\subsection{Booleans}

\subsection{Interval}

\subsection{Function extensionality}

\subsection{Equivalences}

\subsection{Univalence}

\subsection{Natural numbers}

\section{References}

• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. (web, pdf)

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)

• Benno van den Berg, Martijn den Besten?, Quadratic type checking for objective type theory (arXiv:2102.00905)

\section{External links}

• the nLab’s article on homotopy type theory