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 formalsystem of homotopy type theory. Nevertheless, it is important to have aprecise description of homotopy type theory as a formal system in order to, for example,
- •
state and prove its metatheoretic properties, including logicalconsistency,
- •
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 , is not obvious: if we had erroneouslychosen a definition of equivalence for which , thenunivalence would imply that has an element, since does.Nor is it obvious that, for example, our definition of as a higherinductive type yields a type which behaves like the ordinary circle.
There are two aspects of type theory which we must pin down before addressingsuch questions. Recall from the Introduction that type theorycomprises a set of rules specifying when the judgments and hold—for example, products
are characterized by the rule that whenever and , . To make this precise, we must first defineprecisely the syntax of terms—the objects which these judgmentsrelate; then, we must define precisely the judgments and their rules ofinference
—the manner in which judgments can be derived from other judgments.
In this appendix, we present two formulations of Martin-Löf typetheory, and of the extensions that constitute homotopy type theory.The first presentation
(\\autorefsec:syntax-informally) describes the syntax ofterms 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, asis customary in much type-theoretic literature.