3.1 Sets and n-types

In order to explain the connection between the logic of type theoryPlanetmathPlanetmath and the logic of set theoryMathworldPlanetmath, it is helpful to have a notion of set in type theory. While types in general behave like spaces or higher groupoidsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, 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 morphismsMathworldPlanetmathPlanetmath; while topologically, we may consider spaces having the discrete topology. More generally, we may consider groupoids or spaces that are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to ones of this sort; since everything we do in type theory is up to homotopyMathworldPlanetmathPlanetmath, we can’t expect to tell the differencePlanetmathPlanetmath.

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 dimensionsMathworldPlanetmath. Fortunately, because everything in homotopy type theory is automatically functorial/continuousPlanetmathPlanetmath, it turns out to be sufficient to ask this at the bottom level.

Definition 3.1.1.

A type A is a set if for all x,y:A and all p,q:x=y, we have p=q.

More precisely, the propositionPlanetmathPlanetmathPlanetmath 𝗂𝗌𝖲𝖾𝗍(A) 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 predicateMathworldPlanetmath. They are more like the sets used in structural mathematics and in category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath, whose elements are “abstract points” to which we give structureMathworldPlanetmath with functions and relationsMathworldPlanetmathPlanetmathPlanetmath. 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.

Example 3.1.2.

The type 1 is a set. For by Theorem 2.8.1 (http://planetmath.org/28theunittype#S8.Thmthm1), for any x,y:1 the type (x=y) is equivalent to 1. Since any two elements of 1 are equal, this implies that any two elements of x=y are equal.

Example 3.1.3.

The type 0 is a set, for given any x,y:0 we may deduce anything we like, by the inductionMathworldPlanetmath principle of 0.

Example 3.1.4.

The type N of natural numbersMathworldPlanetmath is also a set. This follows from Theorem 2.13.1 (http://planetmath.org/213naturalnumbers#Thmprethm1), since all equality types x=Ny are equivalent to either 1 or 0, and any two inhabitants of 1 or 0 are equal. We will see another proof of this fact in http://planetmath.org/node/87580Chapter 7.

Most of the type forming operationsMathworldPlanetmath we have considered so far also preserve sets.

Example 3.1.5.

If A and B are sets, then so is A×B. For given x,y:A×B and p,q:x=y, by Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1) we have p=pair=(appr1(p),appr2(p)) and q=pair=(appr1(q),appr2(q)). But appr1(p)=appr1(q) since A is a set, and appr2(p)=appr2(q) since B is a set; hence p=q.

Similarly, if A is a set and B:AU is such that each B(x) is a set, then (x:A)B(x) is a set.

Example 3.1.6.

If A is any type and B:AU is such that each B(x) is a set, then the type (x:A)B(x) is a set. For suppose f,g:(x:A)B(x) and p,q:f=g. By function extensionality, we have


But for any x:A, we have

𝗁𝖺𝗉𝗉𝗅𝗒(p,x):f(x)=g(x)  𝑎𝑛𝑑  𝗁𝖺𝗉𝗉𝗅𝗒(q,x):f(x)=g(x),

so since B(x) is a set we have happly(p,x)=happly(q,x). Now using function extensionality again, the dependent functions (xhapply(p,x)) and (xhapply(q,x)) are equal, and hence (applying apfunext) so are p and q.

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 n-types. The next rung consists of 1-types, which are analogous to 1-groupoids in category theory. The defining property of a set (which we may also call a 0-type) is that it has no non-trivial paths. Similarly, the defining property of a 1-type is that it has no non-trivial paths between paths:

Definition 3.1.7.

A type A is a 1-type if for all x,y:A and p,q:x=y and r,s:p=q, we have r=s.

Similarly, we can define 2-types, 3-types, and so on. We will define the general notion of n-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 A is an n-type then A is an (n+1)-type. For example:

Lemma 3.1.8.

If A is a set (that is, isSet(A) is inhabited), then A is a 1-type.


Suppose f:𝗂𝗌𝖲𝖾𝗍(A); then for any x,y:A and p,q:x=y we have f(x,y,p,q):p=q. Fix x, y, and p, and define g:(q:x=y)(p=q) by g(q):f(x,y,p,q). Then for any r:q=q, we have 𝖺𝗉𝖽g(r):r*(g(q))=g(q). By Lemma 1 (http://planetmath.org/211identitytype#Thmlem1), therefore, we have g(q)\centerdotr=g(q).

In particular, suppose given x,y,p,q and r,s:p=q, as in Definition 3.1.7 (http://planetmath.org/31setsandntypes#Thmpredefn2), and define g as above. Then g(p)\centerdotr=g(q) and also g(p)\centerdots=g(q), hence by cancellation r=s. ∎

Second, this stratification of types by level is not degenerate, in the sense that not all types are sets:

Example 3.1.9.

The universePlanetmathPlanetmath U is not a set. To prove this, it suffices to exhibit a type A and a path p:A=A which is not equal to reflA. Take A=2, and let f:AA be defined by f(02):12 and f(12):02. Then f(f(x))=x for all x (by an easy case analysis), so f is an equivalence. Hence, by univalence, f gives rise to a path p:A=A.

If p were equal to reflA, then (again by univalence) f would equal the identity function of A. But this would imply that 02=12, 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 n, there are types which are not n-types.

Note that A is a 1-type exactly when for any x,y:A, the identity type x=Ay 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 n-types we will give in http://planetmath.org/node/87580Chapter 7.

We can also extend this characterization “downwards” from sets. That is, a type A is a set just when for any x,y:A, any two elements of x=Ay are equal. Since sets are equivalently 0-types, it is natural to call a type a (-1)-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