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
-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 ,
[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 and function extensionality for types;
and a few features essential for homotopy type theory:
-
•
the univalence axiom; and
- •
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 \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 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 |
---|---|
\metatable |