3.1 Sets and n-types
In order to explain the connection between the logic of type theory and the logic of set theory, it is helpful to have a notion of set in type theory. While types in general behave like spaces or higher groupoids, there is a subclass of them that behave more like the sets in a traditional set-theoretic system. Categorically, we may consider discrete groupoids, which are determined by a set of objects and only identity morphisms as higher morphisms; while topologically, we may consider spaces having the discrete topology. More generally, we may consider groupoids or spaces that are equivalent to ones of this sort; since everything we do in type theory is up to homotopy, we can’t expect to tell the difference.
Intuitively, we would expect a type to “be a set” in this sense if it has no higher homotopical information: any two parallel paths are equal (up to homotopy), and similarly for parallel higher paths at all dimensions. Fortunately, because everything in homotopy type theory is automatically functorial/continuous, it turns out to be sufficient to ask this at the bottom level.
A type is a set if for all and all , we have .
More precisely, the proposition is defined to be the type
As mentioned in §1.1 (http://planetmath.org/11typetheoryversussettheory), the sets in homotopy type theory are not like the sets in ZF set theory, in that there is no global “membership predicate” . They are more like the sets used in structural mathematics and in category theory, whose elements are “abstract points” to which we give structure with functions and relations. This is all we need in order to use them as a foundational system for most set-based mathematics; we will see some examples in http://planetmath.org/node/87584Chapter 10.
Which types are sets? In http://planetmath.org/node/87580Chapter 7 we will study a more general form of this question in depth, but for now we can observe some easy examples.
The type is a set. For by Theorem 2.8.1 (http://planetmath.org/28theunittype#S8.Thmthm1), for any the type is equivalent to . Since any two elements of are equal, this implies that any two elements of are equal.
The type is a set, for given any we may deduce anything we like, by the induction principle of .
The type of natural numbers is also a set. This follows from Theorem 2.13.1 (http://planetmath.org/213naturalnumbers#Thmprethm1), since all equality types are equivalent to either or , and any two inhabitants of or are equal. We will see another proof of this fact in http://planetmath.org/node/87580Chapter 7.
If and are sets, then so is . For given and , by Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1) we have and . But since is a set, and since is a set; hence .
Similarly, if is a set and is such that each is a set, then is a set.
If is any type and is such that each is a set, then the type is a set. For suppose and . By function extensionality, we have
But for any , we have
so since is a set we have . Now using function extensionality again, the dependent functions and are equal, and hence (applying ) so are and .
For more examples, see http://planetmath.org/node/87828Exercise 3.2,http://planetmath.org/node/87768Exercise 3.3. For a more systematic investigation of the subsystem (category) of all sets in homotopy type theory, see http://planetmath.org/node/87584Chapter 10.
Sets are just the first rung on a ladder of what are called homotopy -types. The next rung consists of -types, which are analogous to -groupoids in category theory. The defining property of a set (which we may also call a -type) is that it has no non-trivial paths. Similarly, the defining property of a -type is that it has no non-trivial paths between paths:
A type is a 1-type if for all and and , we have .
Similarly, we can define -types, -types, and so on. We will define the general notion of -type inductively in http://planetmath.org/node/87580Chapter 7, and study the relationships between them.
However, for now it is useful to have two facts in mind. First, the levels are upward-closed: if is an -type then is an -type. For example:
If is a set (that is, is inhabited), then is a 1-type.
Suppose ; then for any and we have . Fix , , and , and define by . Then for any , we have . By Lemma 1 (http://planetmath.org/211identitytype#Thmlem1), therefore, we have .
In particular, suppose given and , as in Definition 3.1.7 (http://planetmath.org/31setsandntypes#Thmpredefn2), and define as above. Then and also , hence by cancellation . ∎
Second, this stratification of types by level is not degenerate, in the sense that not all types are sets:
The universe is not a set. To prove this, it suffices to exhibit a type and a path which is not equal to . Take , and let be defined by and . Then for all (by an easy case analysis), so is an equivalence. Hence, by univalence, gives rise to a path .
If were equal to , then (again by univalence) would equal the identity function of . But this would imply that , contradicting Remark 1 (http://planetmath.org/212coproducts#Thmrmk1).
In http://planetmath.org/node/87579Chapter 6,http://planetmath.org/node/87582Chapter 8 we will show that for any , there are types which are not -types.
Note that is a 1-type exactly when for any , the identity type is a set. (Thus, Lemma 3.1.8 (http://planetmath.org/31setsandntypes#Thmprelem1) could equivalently be read as saying that the identity types of a set are also sets.) This will be the basis of the recursive definition of -types we will give in http://planetmath.org/node/87580Chapter 7.
We can also extend this characterization “downwards” from sets. That is, a type is a set just when for any , any two elements of are equal. Since sets are equivalently 0-types, it is natural to call a type a -type if it has this latter property (any two elements of it are equal). Such types may be regarded as propositions in a narrow sense, and their study is just what is usually called “logic”; it will occupy us for the rest of this chapter.
|Title||3.1 Sets and n-types|