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.

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 proposition $\mathsf{isSet}(A)$ is defined to be the type

$\mathsf{isSet}(A):\!\!\equiv\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}}\mathchoice{\prod_{(p,q:x=y)}\,}{\mathchoice% {{\textstyle\prod_{(p,q:x=y)}}}{\prod_{(p,q:x=y)}}{\prod_{(p,q:x=y)}}{\prod_{(% p,q:x=y)}}}{\mathchoice{{\textstyle\prod_{(p,q:x=y)}}}{\prod_{(p,q:x=y)}}{% \prod_{(p,q:x=y)}}{\prod_{(p,q:x=y)}}}{\mathchoice{{\textstyle\prod_{(p,q:x=y)% }}}{\prod_{(p,q:x=y)}}{\prod_{(p,q:x=y)}}{\prod_{(p,q:x=y)}}}(p=q).$

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” $\in$ . 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.

Example 3.1.2.

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

Example 3.1.3.

The type $\mathbf{0}$ is a set, for given any $x,y:\mathbf{0}$ we may deduce anything we like, by the induction principle of $\mathbf{0}$ .

Example 3.1.4.

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

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

Example 3.1.5.

If $A$ and $B$ are sets, then so is $A\times B$ . For given $x,y:A\times B$ and $p,q:x=y$ , by Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1) we have $p=\mathsf{pair}^{\mathord{=}}(\mathsf{ap}_{\mathsf{pr}_{1}}(p),\mathsf{ap}_{% \mathsf{pr}_{2}}(p))$ and $q=\mathsf{pair}^{\mathord{=}}(\mathsf{ap}_{\mathsf{pr}_{1}}(q),\mathsf{ap}_{% \mathsf{pr}_{2}}(q))$ . But $\mathsf{ap}_{\mathsf{pr}_{1}}(p)=\mathsf{ap}_{\mathsf{pr}_{1}}(q)$ since $A$ is a set, and $\mathsf{ap}_{\mathsf{pr}_{2}}(p)=\mathsf{ap}_{\mathsf{pr}_{2}}(q)$ since $B$ is a set; hence $p=q$ .

Similarly, if $A$ is a set and $B:A\to\mathcal{U}$ is such that each $B(x)$ is a set, then $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)$ is a set.

Example 3.1.6.

If $A$ is any type and $B:A\to\mathcal{U}$ is such that each $B(x)$ is a set, then the type $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)$ is a set. For suppose $f,g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(% x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)$ and $p,q:f=g$ . By function extensionality, we have

$p={\mathsf{funext}(x\mapsto\mathsf{happly}(p,x))}\quad\text{and}\quad q={% \mathsf{funext}(x\mapsto\mathsf{happly}(q,x))}.$

But for any $x : A$ , we have

$\mathsf{happly}(p,x):f(x)=g(x)\qquad\text{and}\qquad\mathsf{happly}(q,x):f(x)=% g(x),$

so since $B(x)$ is a set we have $\mathsf{happly}(p,x)=\mathsf{happly}(q,x)$ . Now using function extensionality again, the dependent functions $(x\mapsto\mathsf{happly}(p,x))$ and $(x\mapsto\mathsf{happly}(q,x))$ are equal, and hence (applying $\mathsf{ap}_{\mathsf{funext}}$ ) 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, $\mathsf{isSet}(A)$ is inhabited), then $A$ is a 1-type.

Proof.

Suppose $f:\mathsf{isSet}(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:\mathchoice{\prod_{q:x=y}\,}{\mathchoice{{\textstyle\prod_{(q:x=y)}}}{\prod_% {(q:x=y)}}{\prod_{(q:x=y)}}{\prod_{(q:x=y)}}}{\mathchoice{{\textstyle\prod_{(q% :x=y)}}}{\prod_{(q:x=y)}}{\prod_{(q:x=y)}}{\prod_{(q:x=y)}}}{\mathchoice{{% \textstyle\prod_{(q:x=y)}}}{\prod_{(q:x=y)}}{\prod_{(q:x=y)}}{\prod_{(q:x=y)}}% }(p=q)$ by $g(q):\!\!\equiv f(x,y,p,q)$ . Then for any $r:q=q^{\prime}$ , we have $\mathsf{apd}_{g}(r):{r}_{*}\mathopen{}\left({g(q)}\right)\mathclose{}=g(q^{% \prime})$ . By Lemma 1 (http://planetmath.org/211identitytype#Thmlem1), therefore, we have $g(q)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}r=g(q^{\prime})$ .

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)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}r=g(q)$ and also $g(p)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}s=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 universe $\mathcal{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 $\mathsf{refl}_{A}$ . Take $A=\mathbf{2}$ , and let $f:A\to A$ be defined by $f({0_{\mathbf{2}}}):\!\!\equiv{1_{\mathbf{2}}}$ and $f({1_{\mathbf{2}}}):\!\!\equiv{0_{\mathbf{2}}}$ . 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 $\mathsf{refl}_{A}$ , then (again by univalence) $f$ would equal the identity function of $A$ . But this would imply that ${0_{\mathbf{2}}}={1_{\mathbf{2}}}$ , 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=_{A}y$ 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=_{A}y$ 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
\metatable