A. Formal type theory

Just as one can develop mathematics in set theoryMathworldPlanetmath 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:𝟎, is not obvious: if we had erroneously chosen a definition of equivalence for which 𝟎𝟏, then univalence would imply that 𝟎 has an element, since 𝟏 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 theoryPlanetmathPlanetmath 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 aa:A hold—for example, productsPlanetmathPlanetmathPlanetmath are characterized by the rule that whenever a:A and b:B, (a,b):A×B. To make this precise, we must first define precisely the syntax of terms—the objects a,a,A, which these judgments relate; then, we must define precisely the judgments and their rules of inferenceMathworldPlanetmath—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 extensionsPlanetmathPlanetmathPlanetmath that constitute homotopy type theory. The first presentationMathworldPlanetmathPlanetmath (\autorefsec:syntax-informally) describes the syntax of terms and the forms of judgments as an extension of the untyped λ-calculus, while leaving the rules of inference informal. The second (\autorefsec: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