Chapter 1 notes
The type theory^{} presented here is a version of Martin-Löf’s intuitionistic type theory [14],[16],[18],[20], which itself is based on and influenced by the foundational work of Brouwer [1], Heyting [8], Scott [scott70], de Bruijn [7], Howard [10], Tait [26],[28], and Lawvere [11]. Three principal variants of Martin-Löf’s type theory underlie the NuPRL [3], Coq [5], and Agda [23] computer implementations of type theory. The theory given here differs from these formulations in a number of respects, some of which are critical to the homotopy interpretation^{}, while others are technical conveniences or involve concepts^{} that have not yet been studied in the homotopical setting.
Most significantly, the type theory described here is derived from the intensional version of Martin-Löf’s type theory [16], rather than the extensional version [18]. Whereas the extensional theory makes no distinction between judgmental and propositional equality, the intensional theory regards judgmental equality as purely definitional, and admits a much broader, proof-relevant interpretation of the identity type that is central to the homotopy interpretation. From the homotopical perspective, extensional type theory confines itself to homotopically discrete sets (see §3.1 (http://planetmath.org/31setsandntypes)), whereas the intensional theory admits types with higher-dimensional structure. The NuPRL system [3] is extensional, whereas both Coq [5] and Agda [23] are intensional. Among intensional type theories, there are a number of variants that differ in the structure of identity^{} proofs. The most liberal interpretation, on which we rely here, admits a proof-relevant interpretation of equality, whereas more restricted variants impose restrictions^{} such as uniqueness of identity proofs (UIP) [25], stating that any two proofs of equality are judgmentally equal, and Axiom K [25], stating that the only proof of equality is reflexivity^{} (up to judgmental equality). These additional requirements may be selectively imposed in the Coq and Agda systems.
Another point of variation among intensional theories is the strength of judgmental equality, particularly as regards objects of function type. Here we include the uniqueness principle ($\eta $-conversion) $f\equiv \lambda x.f(x)$, as a principle of judgmental equality. This principle is used, for example, in §4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality), to show that univalence implies propositional function extensionality. Uniqueness principles are sometimes considered for other types. For instance, the uniqueness principle for cartesian products would be a judgmental version of the propositional equality $\mathrm{\U0001d5ce\U0001d5c9\U0001d5c9\U0001d5cd}$ which we constructed in §1.5 (http://planetmath.org/15producttypes), saying that $u\equiv ({\mathrm{\U0001d5c9\U0001d5cb}}_{1}(u),{\mathrm{\U0001d5c9\U0001d5cb}}_{2}(u))$. This and the corresponding version for dependent pairs would be reasonable choices (which we did not make), but we cannot include all such rules, because the corresponding uniqueness principle for identity types would trivialize all the higher homotopical structure. So we are forced to leave it out, and the question then becomes where to draw the line. With regards to inductive types, we discuss these points further in §5.5 (http://planetmath.org/55homotopyinductivetypes).
It is important for our purposes that (propositional) equality of functions is taken to be extensional (in a different sense than that used above!). This is not a consequence of the rules in this chapter; it will be expressed by Axiom 1 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmaxiom1). This decision is significant for our purposes, because it specifies that equality of functions is as expected in mathematics. Although we include Axiom 1 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmaxiom1) as an axiom, it may be derived from the univalence axiom and the uniqueness principle for functions (see §4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality)), as well as from the existence of an interval type (see Lemma 6.3.2 (http://planetmath.org/63theinterval#Thmprelem2)).
Regarding inductive types such as products^{}, $\mathrm{\Sigma}$-types, coproducts, natural numbers^{}, and so on (see http://planetmath.org/node/87578Chapter 5), there are additional choices regarding precisely how to formulate induction^{} and recursion. Formally, one may describe type theory by taking either pattern matching or induction principles as basic and deriving the other; see http://planetmath.org/node/87881Appendix A. However, pattern matching in general is not yet well understood from the homotopical perspective (in particular, “nested” or “deep” pattern matching is difficult to make general sense of for higher inductive types). Moreover, it can be dangerous unless sufficient care is taken: for instance, the form of pattern matching implemented by default in Agda allows proving Axiom K. For these reasons, we have chosen to regard the induction principle as the basic property of an inductive definition, with pattern matching justified in terms of induction.
Unlike the type theory of Coq, we do not include a primitive type of propositions. Instead, as discussed in §1.11 (http://planetmath.org/111propositionsastypes), we embrace the propositions-as-types (PAT) principle, identifying propositions^{} with types. This was suggested originally by de Bruijn [7], Howard [10], Tait [28], and Martin-Löf [14]. (Our decision is explained more fully in §3.2 (http://planetmath.org/32propositionsastypes),§3.3 (http://planetmath.org/33merepropositions).)
We do, however, include a full cumulative hierarchy of universes^{}, so that the type formation and equality judgments become instances of the membership and equality judgments for a universe. As a convenience, we regard objects of a universe as types, rather than as codes for types; in the terminology of [20], this means we use “Russell-style universes” rather than “Tarski-style universes”. An alternative would be to use Tarski-style universes, with an explicit coercion function required to make an element $A:\mathcal{U}$ of a universe into a type $\mathrm{\U0001d5a4\U0001d5c5}(A)$, and just say that the coercion is omitted when working informally.
We also treat the universe hierarchy as cumulative, in that every type in ${\mathcal{U}}_{i}$ is also in ${\mathcal{U}}_{j}$ for each $j\ge i$. There are different ways to implement cumulativity formally: the simplest is just to include a rule that if $A:{\mathcal{U}}_{i}$ then $A:{\mathcal{U}}_{j}$. However, this has the annoying consequence that for a type family $B:A\to {\mathcal{U}}_{i}$ we cannot conclude $B:A\to {\mathcal{U}}_{j}$, although we can conclude $\lambda a.B(a):A\to {\mathcal{U}}_{j}$. A more sophisticated approach that solves this problem is to introduce a judgmental subtyping relation^{} $$ generated by $$, but this makes the type theory more complicated to study. Another alternative would be to include an explicit coercion function $\uparrow :{\mathcal{U}}_{i}\to {\mathcal{U}}_{j}$, which could be omitted when working informally.
It is also not necessary that the universes be indexed by natural numbers and linearly ordered. For some purposes, it is more appropriate to assume only that every universe is an element of some larger universe, together with a “directedness” property that any two universes are jointly contained in some larger one. There are many other possible variations, such as including a universe “${\mathcal{U}}_{\omega}$” that contains all ${\mathcal{U}}_{i}$ (or even higher “large cardinal” type universes), or by internalizing the hierarchy into a type family $\lambda i.{\mathcal{U}}_{i}$. The latter is in fact done in Agda.
The path induction principle for identity types was formulated by Martin-Löf [14]. The based path induction rule in the setting of Martin-Löf type theory is due to Paulin-Mohring [21]; it can be seen as an intensional generalization^{} of the concept of “pointwise functionality” for hypothetical judgments from NuPRL [3, Section^{} 8.1]. The fact that Martin-Löf’s rule implies Paulin-Mohring’s was proved by Streicher using Axiom K (see §7.2 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem)), by Altenkirch and Goguen as in §1.12 (http://planetmath.org/112identitytypes), and finally by Hofmann without universes (as in http://planetmath.org/node/87560Exercise 1.7); see [25], §1.3 (http://planetmath.org/13universesandfamilies) and Addendum.
References
- 1 Beeson,Michael, Foundations of Constructive Mathematics Springer,1985
- 2 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
- 3 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
- 4 Coq Development Team, The Coq Proof Assistant Reference Manual INRIA-Rocquencourt,2012
- 5 Coq Development Team, The Coq Proof Assistant Reference Manual INRIA-Rocquencourt,2012
- 6 de Bruijn,Nicolaas Govert, AUTOMATH,a language^{} for mathematics Les Presses de l’Université de Montréal,Montreal,Quebec,1973
- 7 de Bruijn,Nicolaas Govert, AUTOMATH,a language for mathematics Les Presses de l’Université de Montréal,Montreal,Quebec,1973
- 8 Heyting,Arend, Intuitionism: an introduction North-Holland Pub. Co.,1966
- 9 Howard,William A.. The formulae-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic^{},Lambda Calculus^{} and Formalism,pages 479–490. Academic Press, 1980.
- 10 Howard,William A.. The formulae-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic,Lambda Calculus and Formalism,pages 479–490. Academic Press, 1980.
- 11 F. William Lawvere. Adjointness in Foundations. Reprints in Theory and Applications of Categories, 16:1–16 2006
- 12 Martin-Löf,Per. An intuitionistic theory of types. In Twenty-five years of constructive type theory (Venice,1995),volume 36 of Oxford Logic Guides, pages 127–172. Oxford University Press, 1998.
- 13 Martin-Löf,Per. An intuitionistic theory of types. In Twenty-five years of constructive type theory (Venice,1995),volume 36 of Oxford Logic Guides, pages 127–172. Oxford University Press, 1998.
- 14 Martin-Löf,Per. An intuitionistic theory of types. In Twenty-five years of constructive type theory (Venice,1995),volume 36 of Oxford Logic Guides, pages 127–172. Oxford University Press, 1998.
- 15 Martin-Löf,Per. An intuitionistic theory of types: predicative part. In Logic Colloquium ’73,Proceedings of the Logic Colloquium,volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73–118. North-Holland, 1975.
- 16 Martin-Löf,Per. An intuitionistic theory of types: predicative part. In Logic Colloquium ’73,Proceedings of the Logic Colloquium,volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73–118. North-Holland, 1975.
- 17 Martin-Löf,Per. Constructive mathematics and computer programming. In Logic,Methodology and Philosophy of Science VI,Proceedings of the Sixth International Congress of Logic,Methodology and Philosophy of Science,Hannover 1979,volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153–175. North-Holland, 1982.
- 18 Martin-Löf,Per. Constructive mathematics and computer programming. In Logic,Methodology and Philosophy of Science VI,Proceedings of the Sixth International Congress of Logic,Methodology and Philosophy of Science,Hannover 1979,volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153–175. North-Holland, 1982.
- 19 Martin-Löf,Per, Intuitionistic type theory Bibliopolis,1984
- 20 Martin-Löf,Per, Intuitionistic type theory Bibliopolis,1984
- 21 Christine Paulin-Mohring. Inductive Definitions in the System Coq - Rules and Properties. In emphProceedings of the conference Typed Lambda Calculi and Applications, .
- 22 Norell,Ulf. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers,Göteborg University, 2007.
- 23 Norell,Ulf. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers,Göteborg University, 2007.
- 24 Thomas Streicher. Investigations into intensional type theory, 1993. Habilitationsschrift,Ludwig-Maximilians-Universität München.
- 25 Thomas Streicher. Investigations into intensional type theory, 1993. Habilitationsschrift,Ludwig-Maximilians-Universität München.
- 26 Tait,William W.. Intensional interpretations of functionals^{} of finite type. I. The Journal of Symbolic Logic, 32:198–212 1967
- 27 Tait,William W.. Constructive reasoning. In Logic,Methodology and Philos. Sci. III (Proc. Third Internat. Congr.,Amsterdam,1967),pages 185–199. North-Holland, 1968.
- 28 Tait,William W.. Constructive reasoning. In Logic,Methodology and Philos. Sci. III (Proc. Third Internat. Congr.,Amsterdam,1967),pages 185–199. North-Holland, 1968.
Title | Chapter 1 notes |
---|---|
\metatable |