Appendix A Notes

The system of rules with introduction (primitive constants) and eliminationand computation rules (defined constant) is inspired by Gentzen naturaldeduction. The possibility of strengthening the elimination rule forexistential quantification was indicated in [howard:pat]. Thestrengthening of the axioms for disjunction appears in [Martin-Lof-1972],and for absurdity elimination and identity type in [Martin-Lof-1973]. The$W$-types were introduced in [Martin-Lof-1979]. They generalize a notionof trees introduced by [Tait-1968].

The generalized form of primitive recursion for natural numbers and ordinalsappear in [Hilbert-1925]. This motivated Gödel’s system $T$,[Goedel-T-1958], which was analyzed by [Tait-1966], who used,following [Goedel-T-1958], the terminology “definitional equality” forconversion: two terms are judgmentally equal if they reduce to acommon term by means of a sequence of applications of the reductionrules. This terminology was also used by de Bruijn [deBruijn-1973] in hispresentation of AUTOMATH.

Streicher [Streicher-1991, Theorem 4.13], explains how to give thesemantics in a contextual category of terms in normal form using a simple syntaxsimilar to the one we have presented.

Our second presentation comprises fairly standard presentation ofintensional Martin-Löf type theory, with some additional features needed inhomotopy type theory. Compared to a reference presentation of[hofmann:syntax-and-semantics], the type theory of this book has a fewnon-critical differences:

• universes à la Russell, in the sense of[martin-lof:bibliopolis]; and

• judgmental $\eta$ and function extensionality for $\mathrm{\Pi }$ types;

and a few features essential for homotopy type theory:

• the univalence axiom; and

• higher inductive types.

As a matter of convenience, the book primarily defines functions by inductionusing definition by pattern matching.It is possible to formalize thenotion of pattern matching, as done in sec:syntax-informally. However, thestandard type-theoretic presentation, adopted in sec:syntax-more-formally, is to introduce a single dependenteliminator for each type former, from which functions out of that type must bedefined. This approach is easier to formalize both syntactically andsemantically, as it amounts to the universal property of the type former.The two approaches are equivalent; see §1.10 (http://planetmath.org/110patternmatchingandrecursion) for alonger discussion.