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{\U0001d5ab\U0001d5a4\U0001d5ac}$ 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].
References
- 1 Awodey,Steven and Bauer,Andrej. Propositions as [types]. Journal of Logic and Computation, 14:447–471 2004,Bdsk-Url-1
- 2 Aczel,Peter and Gambino,Nicola. Collection^{} principles in dependent type theory. In emphTypes for Proofs and Programs,International Workshop,TYPES 2000,Durham,UK,December 8-12,2000,Selected Papers, pages 1–23Springer, .
- 3 Aczel,Peter and Gambino,Nicola. Collection principles in dependent type theory. In emphTypes for Proofs and Programs,International Workshop,TYPES 2000,Durham,UK,December 8-12,2000,Selected Papers, pages 1–23Springer, .
- 4 Constable,Robert L.. Constructive Mathematics as a Programming Logic I: Some Principles of Theory. In Annals of Mathematics,volume 24 pages 21–37. Elsevier Science Publishers,B.V. (North-Holland), 1985.
- 5 Robert L. Constable and Stuart F. Allen and H. M. Bromley and W. R. Cleaveland and J. F. Cremer and Robert W. Harper and Douglas J. Howe and T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and Scott F. Smith, Implementing Mathematics with the NuPRL Proof Development System Prentice Hall,1986
- 6 Peter T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2 Oxford Science Publications,2002
- 7 Bart Jacobs, Categorical logic and type theory Elsevier,1999
- 8 Maietti,Maria Emilia and Sambin,Giovanni. Toward a minimalist foundation for constructive mathematics. In From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics,volume 48 of Oxford Logic Guides, pages 91–114. Clarendon Press, 2005.
- 9 Martin-Löf,Per. 100 years of Zermelo’s axiom of choice: what was the problem with it?. The Computer Journal, 49:345–350 2006
- 10 Whitehead,Alfred North and Russell,Bertrand, Principia mathematica,3 vol.s Cambridge University Press,1910–1913; Second edition,1925–1927
- 11 Arnaud Spiwack. A Journey Exploring the Power and Limits of Dependent Type Theory. PhD thesis, École Polytechnique,Palaiseau,France, 2011.
- 12 Troelstra,Anne Sjerp and van Dalen,Dirk, Constructivism in mathematics. Vol. I North-Holland Publishing Co.,1988
- 13 Troelstra,Anne Sjerp and van Dalen,Dirk, Constructivism in mathematics. Vol. II North-Holland Publishing Co.,1988
- 14 Vladimir Voevodsky. A universe^{} polymorphic type system. \urlhttp://uf-ias-2012.wikispaces.com/file/view/Universe+polymorphic+type+sytem.pdf, 2012.
Title | Chapter 3 Notes |
---|---|
\metatable |