# 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.

###### 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