A. Formal type theory

Just as one can develop mathematics in set theory without explicitly using the axioms of Zermelo–Fraenkel set theory, in this book we have developed mathematics in univalent foundations without explicitly referring to a formal system of homotopy type theory. Nevertheless, it is important to have a precise description of homotopy type theory as a formal system in order to, for example,

• state and prove its metatheoretic properties, including logical consistency,

• construct models, e.g. in simplicial sets, model categories, higher toposes, etc., and

• implement it in proof assistants like Coq or Agda.

Even the logical consistency of homotopy type theory, namely that in the empty context there is no term $a:\mathrm{𝟎}$, is not obvious: if we had erroneously chosen a definition of equivalence for which $\mathrm{𝟎}\simeq \mathrm{𝟏}$, then univalence would imply that $\mathrm{𝟎}$ has an element, since $\mathrm{𝟏}$ does. Nor is it obvious that, for example, our definition of ${𝕊}^1$ as a higher inductive type yields a type which behaves like the ordinary circle.

There are two aspects of type theory which we must pin down before addressing such questions. Recall from the Introduction that type theory comprises a set of rules specifying when the judgments $a:A$ and $a\equiv a^{\prime }:A$ hold—for example, products are characterized by the rule that whenever $a:A$ and $b:B$, $(a,b):A\times B$. To make this precise, we must first define precisely the syntax of terms—the objects $a,a^{\prime },A,\mathrm{\dots }$ which these judgments relate; then, we must define precisely the judgments and their rules of inference—the manner in which judgments can be derived from other judgments.

In this appendix, we present two formulations of Martin-Löf type theory, and of the extensions that constitute homotopy type theory. The first presentation (sec:syntax-informally) describes the syntax of terms and the forms of judgments as an extension of the untyped $\lambda$-calculus, while leaving the rules of inference informal. The second (sec:syntax-more-formally) defines the terms, judgments, and rules of inference inductively in the style of natural deduction, as is customary in much type-theoretic literature.

Title	A. Formal type theory