Chapter 3 Notes

The fact that it is possible to define sets, mere propositions, and contractible types in type theory, with all higher homotopies automatically taken care of as in §3.1 (http://planetmath.org/31setsandntypes),§3.3 (http://planetmath.org/33merepropositions),§3.11 (http://planetmath.org/311contractibility), was first observed by Voevodsky. In fact, he defined the entire hierarchy of $n$-types by induction, as we will do in http://planetmath.org/node/87580Chapter 7.

Theorem 3.2.2 (http://planetmath.org/32propositionsastypes#Thmprethm1),Corollary 3.2.7 (http://planetmath.org/32propositionsastypes#Thmprecor1) rely in essence on a classical theorem of Hedberg, which we will prove in §7.2 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem). The implication that the propositions-as-types form of $\mathrm{𝖫𝖤𝖬}$ contradicts univalence was observed by Martín Escardó on the Agda mailing list. The proof we have given of Theorem 3.2.2 (http://planetmath.org/32propositionsastypes#Thmprethm1) is due to Thierry Coquand.

The propositional truncation was introduced in the extensional type theory of NuPRL in 1983 by Constable [4] as an application of “subset” and “quotient” types. What is here called the “propositional truncation” was called “squashing” in the NuPRL type theory [5]. Rules characterizing the propositional truncation directly, still in extensional type theory, were given in [1]. The intensional version in homotopy type theory was constructed by Voevodsky using an impredicative quantification, and later by Lumsdaine using higher inductive types (see §6.9 (http://planetmath.org/69truncations)).

Voevodsky [14] has proposed resizing rules of the kind considered in §3.5 (http://planetmath.org/35subsetsandpropositionalresizing). These are clearly related to the notorious axiom of reducibility proposed by Russell in his and Whitehead’s Principia Mathematica [10].

The adverb “purely” as used to refer to untruncated logic is a reference to the use of monadic modalities to model effects in programming languages; see §7.7 (http://planetmath.org/77modalities) and the Notes to http://planetmath.org/node/87580Chapter 7.

There are many different ways in which logic can be treated relative to type theory. For instance, in addition to the plain propositions-as-types logic described in §1.11 (http://planetmath.org/111propositionsastypes), and the alternative which uses mere propositions only as described in §3.6 (http://planetmath.org/36thelogicofmerepropositions), one may introduce a separate “sort” of propositions, which behave somewhat like types but are not identified with them. This is the approach taken in logic enriched type theory [3] and in some presentations of the internal languages of toposes and related categories (e.g. [7],[6]), as well as in the proof assistant Coq. Such an approach is more general, but less powerful. For instance, the principle of unique choice (§3.9 (http://planetmath.org/39theprincipleofuniquechoice)) fails in the category of so-called setoids in Coq [11], in logic enriched type theory [3], and in minimal type theory [8]. Thus, the univalence axiom makes our type theory behave more like the internal logic of a topos; see also http://planetmath.org/node/87584Chapter 10.

Martin-Löf [9] provides a discussion on the history of axioms of choice. Of course, constructive and intuitionistic mathematics has a long and complicated history, which we will not delve into here; see for instance [12],[13].

Title	Chapter 3 Notes