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 disjunctionMathworldPlanetmath 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 numbersMathworldPlanetmath and ordinalsMathworldPlanetmathPlanetmath 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 sequencePlanetmathPlanetmath of applications of the reductionPlanetmathPlanetmathPlanetmath rules. This terminology was also used by de Bruijn [deBruijn-1973] in his presentationMathworldPlanetmathPlanetmath of AUTOMATH.

Streicher [Streicher-1991, TheoremMathworldPlanetmath 4.13], explains how to give the semantics in a contextual categoryMathworldPlanetmath 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 theoryPlanetmathPlanetmath, 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 differencesPlanetmathPlanetmath:

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

  • judgmental η and function extensionality for Π types;

and a few features essential for homotopy type theory:

As a matter of convenience, the book primarily defines functions by inductionMathworldPlanetmath using definition by pattern matching. It is possible to formalize the notion of pattern matching, as done in \autorefsec:syntax-informally. However, the standard type-theoretic presentation, adopted in \autorefsec: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 propertyMathworldPlanetmath of the type former. The two approaches are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath; see §1.10 (http://planetmath.org/110patternmatchingandrecursion) for a longer discussion.

Title Appendix A Notes
\metatable