\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. In a similar manner, for simplicity and ease of presentation, we shall also follow the HoTT book in not including a separate $A \; \mathrm{type}$ judgment and rather stipulating that every type is an element of a Russell universe. \subsection{Judgments and contexts} We introduce two judgments in the model: typing judgments, where we judge $a$ to be an element of $A$, $a:A$, and context judgments, where we judge $\Gamma$ to be a context, $\Gamma \; \mathrm{ctx}$. Contexts are lists of typing judgments $a:A$, $b:B$, $c:C$, et cetera, and are formalized by the rules for the empty context and extending the context by a typing judgment $$\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A:\mathrm{U}_i}{(\Gamma, a:A) \; \mathrm{ctx}}$$ \subsection{Structural rules} The variable rule states that we may derive a typing judgment if the typing judgment is in the context already: $$\frac{\vdash \Gamma, a:A, \Delta \; \mathrm{ctx}}{\vdash \Gamma, a:A, \Delta \vdash a:A}$$ Let $\mathcal{J}$ be any arbitrary judgment. Then we have the following rules: The weakening rule: $$\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A:\mathcal{U}_i}{\Gamma, a:A, \Delta \vdash \mathcal{J}}$$ The substitution rule: $$\frac{\Gamma \vdash a:A \quad \Gamma, b:A, \Delta \vdash \mathcal{J}}{\Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}$$ The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations. \subsection{Russell universes} Universes are the types of types in type theory. We introduce a hierarchy of universes $U_i$ indexed by natural numbers $i$ in the metatheory, with rules for universe formation and cumulativity. $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash U_i : U_{i + 1}} \qquad \frac{\Gamma \vdash A:U_i}{\Gamma \vdash A:U_{i + 1}}$$ \subsection{Sections and dependent types} A section is a term $b:B$ in the context of the variable judgment $x:A$, $x:A \vdash b:B$. Sections are usually written as $b(x)$ to indicate its dependence upon $x$. A dependent type is a section of a universe $B:U_i$ in the context of the variable judgment $x:A$, $x:A \vdash B:U_i$, and since they are sections, they are usually written as $B(x)$. \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. Equality comes with a formation rule, an introduction rule, an elimination rule, and a computation rule: Formation rule for identity types: $$\frac{\Gamma \vdash A:U_i}{\Gamma, a:A, b:A \vdash a =_A b:U_i}$$ Introduction rule for identity types: $$\frac{\Gamma \vdash A:U_i}{\Gamma, a:A \vdash \mathrm{refl}_A(a) : a =_A a}$$ Elimination rule for identity types: $$\frac{\Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash C(a, b, p):U_i \quad \Gamma, a:A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t:C(a, a, \mathrm{refl}_A(a))}{\Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash J(t, a, b, p):C(a, b, p)}$$ Computation rules for identity types: $$\frac{\Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash C(a, b, p):U_i \quad \Gamma, a:A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t:C(a, a, \mathrm{refl}_A(a))}{\Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash \beta_{=_A}(a) : J(t, a, a, \mathrm{refl}(a)) =_{C(a, a, \mathrm{refl}_A(a))} t}$$ \subsection{Definitions} In mathematics, many times one would want to define an element to be another element of a type. In order to define an element $a:A$ to be an element $b:A$, one says that element $a:A$ comes with an identification $\mathrm{def}(a):a =_A b$. Since types are elements of universes, one defines a type $A:\mathcal{U}_i$ to be a type $B:\mathcal{U}_i$ if the type $A:\mathcal{U}_i$ comes with an identification $\mathrm{def}(A):A =_{\mathcal{U}_i} B$. Sometimes, for ease of simplicity, the identity type is simply written $a = b$ for elements $a:A$ and $b:A$. The type argument $A$ for the identity type then becomes an **implicit argument**. Thus, in order to define $a$ to be $b$, one says that $a$ comes with an identification $\mathrm{def}(a):a = b$. In a proof assistant or some other program, **elaboration** is needed to expand out all the implicit arguments to get the right type $a =_A b$. \subsection{Natural numbers} Formation rules for the natural numbers: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N}:U_i}$$ Introduction rules for the natural numbers: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \vdash n:\mathbb{N}}{\Gamma \vdash s(n):\mathbb{N}}$$ Elimination rules for the natural numbers: $$\frac{\Gamma, x:\mathbb{N} \vdash C(x):U_i \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c(x):C(x) \vdash c_s(x, c(x)):C(s(x)) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{ind}_C^n(c_0, c_s):C(n)}$$ Computation rules for the natural numbers: $$\frac{\Gamma, x:\mathbb{N} \vdash C(x):U_i \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c(x):C(x) \vdash c_s(x, c(x)):C(s(x))}{\Gamma \vdash \beta_\mathrm{N}^{0}: \mathrm{ind}_C^0(c_0, c_s) =_{C(0)} c_0}$$ $$\frac{\Gamma, x:\mathbb{N} \vdash C(x):U_i \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c(x):C(x) \vdash c_s(x, c(x)):C(s(x))}{\Gamma \vdash \beta_\mathrm{N}^{s}: \mathrm{ind}_C^{s(n)}(c_0, c_s) =_{C(s(n))} c_s(n, \mathrm{ind}_C^{n}(c_0, c_s))}$$ Uniqueness rules for the natural numbers: ... \subsection{Function types} Formation rules for function types: $$\frac{\Gamma \vdash A:U_i \quad \Gamma \vdash B:U_i}{\Gamma \vdash A \to B:U_i}$$ Introduction rules for function types: $$\frac{\Gamma, x:A \vdash b(x):B}{\Gamma \vdash (x \mapsto b(x)):A \to B}$$ Elimination rules for function types: $$\frac{\Gamma \vdash f:A \to B \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B}$$ Computation rules for function types: $$\frac{\Gamma, x:A \vdash b(x):B \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\to}:(x \mapsto b(x))(a) =_{B} b}$$ Uniqueness rules for function types: $$\frac{\Gamma \vdash f:A \to B}{\Gamma \vdash \eta_{\to}:f =_{A \to B} (x \to f(x))}$$ \subsection{Pi types} Pi types are the dependent versions of functions or products, depending on how one looks at it. Formation rules for Pi types: $$\frac{\Gamma \vdash A:U_i \quad \Gamma, x:A \vdash B(x):U_i}{\Gamma \vdash \Pi(x:A).B(x):U_i}$$ Introduction rules for Pi types: $$\frac{\Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\Pi(x:A).B(x)}$$ Elimination rules for Pi types: $$\frac{\Gamma \vdash f:\Pi(x:A).B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B[a/x]}$$ Computation rules for Pi types: $$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_\Pi:\lambda(x:A).b(x)(a) =_{B[a/x]} b[a/x]}$$ Uniqueness rules for Pi types: $$\frac{\Gamma \vdash f:\Pi(x:A).B(x)}{\Gamma \vdash \eta_\Pi:f =_{\Pi(x:A).B(x)} \lambda(x).f(x)}$$ \subsection{Product types} \subsection{Sigma types} We use the negative presentation for sigma types. Formation rules for Sigma types: $$\frac{\Gamma \vdash A:U_i \quad \Gamma, x:A \vdash B(x):U_i}{\Gamma \vdash \Sigma(x:A).B(x):U_i}$$ Introduction rules for Sigma types: $$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B[a/x]}{\Gamma \vdash (a, b):\Sigma(x:A).B(x)}$$ Elimination rules for Sigma types: $$\frac{\Gamma \vdash z:\Sigma(x:A).B(x)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\Sigma(x:A).B(x)}{\Gamma \vdash \pi_2(z):B(\pi_1(z))}$$ Computation rules for Sigma types: $$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\Sigma 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma, x:A \vdash b:B \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\Sigma 2}:\pi_2(a, b) =_{B\pi_1(a, b)} b}$$ Uniqueness rules for Sigma types: $$\frac{\Gamma \vdash z:\Sigma(x:A).B(x)}{\Gamma \vdash \eta_\Sigma:z =_{\Sigma(x:A).B(x)} (\pi_1(z), \pi_2(z))}$$ \subsection{Sum types} \subsection{Empty type} \subsection{Unit type} \subsection{Boolean type} \subsection{Interval type} \subsection{Function extensionality} \subsection{Singletons} A singleton is a type with only one element up to identifications. We define the function $\mathrm{isSingl}:U_i \to U_i$ which states that a type $A:U_i$ is a singleton if there is an identification $$\mathrm{def}(\mathrm{isSingl})(A):\mathrm{isSingl}(A) =_{U_i} \Sigma(a:A).\Pi(b:A).a =_A b$$ \subsection{Fibers} Given types $A:U_i$ and $B:U_i$ let the type family $$\mathrm{fiber}(A, B):((A \to B) \times B) \to U_i$$ comes with identifications $$\mathrm{def}(\mathrm{fiber}(A, B))(f, b):\mathrm{fiber}(A, B)(f, b) =_{U_i} \Sigma(a:A).f(a) =_B b$$ for each function $f:A \to B$ and element $b:B$. The type $\mathrm{fiber}(A, B)(f, b)$ is known as the fiber of $f$ at $b$. \subsection{Equivalences} We define the type family $(-)\simeq_{U_i}(-):(U_i \times U_i) \to U_i$ such that it comes with identifications $$\mathrm{def}(\simeq_{U_i})(A, B): (A \simeq_{U_i} B) =_{U_i} \Sigma(f:A \to B).\Pi(b:B).\mathrm{isSingl}(\mathrm{fiber}(A, B)(f, b))$$ for all types $A:U_i$ and $B:U_i$. The type $A \simeq_{U_i} B$ is known as the type of equivalences between $A$ and $B$. \subsection{Univalence} \section{References} * *Homotopy Type Theory: Univalent Foundations of Mathematics*, The Univalent Foundations Program, Institute for Advanced Study, 2013. ([web](http://homotopytypetheory.org/book/), [pdf](http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf)) * Egbert Rijke, *Introduction to Homotopy Type Theory*, Cambridge Studies in Advanced Mathematics, Cambridge University Press ([pdf](https://raw.githubusercontent.com/martinescardo/HoTTEST-Summer-School/main/HoTT/hott-intro.pdf)) (478 pages) * Benno van den Berg, Martijn den Besten, *Quadratic type checking for objective type theory* ([arXiv:2102.00905](https://arxiv.org/abs/2102.00905)) \section{External links} * the nLab's article on [[nlab:homotopy type theory]] category:redirected to nlab