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{\U0001d7ce}$, is not obvious: if we had erroneously chosen a definition of equivalence for which $\mathrm{\U0001d7ce}\simeq \mathrm{\U0001d7cf}$, then univalence would imply that $\mathrm{\U0001d7ce}$ has an element, since $\mathrm{\U0001d7cf}$ does. Nor is it obvious that, for example, our definition of ${\mathbb{S}}^{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 MartinLöf type theory, and of the extensions^{} that constitute homotopy type theory. The first presentation^{} (\autorefsec:syntaxinformally) 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 (\autorefsec:syntaxmoreformally) defines the terms, judgments, and rules of inference inductively in the style of natural deduction, as is customary in much typetheoretic literature.
Title  A. Formal type theory 

\metatable 