Appendix A Notes

The system of rules with introduction (primitive constants) and elimination and computation rules (defined constant) is inspired by Gentzen natural deduction. The possibility of strengthening the elimination rule for existential quantification was indicated in [howard:pat]. The strengthening 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 notion of trees introduced by [Tait-1968].

The generalized form of primitive recursion for natural numbers and ordinals appear 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” for conversion: two terms are judgmentally equal if they reduce to a common term by means of a sequence of applications of the reduction rules. This terminology was also used by de Bruijn [deBruijn-1973] in his presentation of AUTOMATH.

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

Our second presentation comprises fairly standard presentation of intensional Martin-Löf type theory, with some additional features needed in homotopy type theory. Compared to a reference presentation of [hofmann:syntax-and-semantics], the type theory of this book has a few non-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 induction using definition by pattern matching. It is possible to formalize the notion of pattern matching, as done in sec:syntax-informally. However, the standard type-theoretic presentation, adopted in sec:syntax-more-formally, is to introduce a single dependent eliminator for each type former, from which functions out of that type must be defined. This approach is easier to formalize both syntactically and semantically, as it amounts to the universal property of the type former. The two approaches are equivalent; see §1.10 (http://planetmath.org/110patternmatchingandrecursion) for a longer discussion.

Title	Appendix A Notes