7.1 Definition of n-types

As mentioned in §3.1 (http://planetmath.org/31setsandntypes),§3.11 (http://planetmath.org/311contractibility), it turns out to be convenient to define $n$-types starting two levels below zero, with the $(-1)$-types being the mere propositions and the $(-2)$-types the contractible ones.

Definition 7.1.1.

Define the predicate $\mathrm{is}\mathit{}\mathit{\text{-}}\mathit{}n\mathit{}\mathit{\text{-}}\mathit{}\mathrm{type}\mathrm{:}\mathrm{U}\mathrm{\to }\mathrm{U}$ for $n\mathrm{\ge }\mathrm{-}\mathrm{2}$ by recursion as follows:

We say that $X$ is an $n$-type, or sometimes that it is $n$-truncated, if $\mathrm{is}\mathit{}\mathit{\text{-}}\mathit{}n\mathit{}\mathit{\text{-}}\mathit{}\mathrm{type}\mathit{}\mathrm{(}X\mathrm{)}$ is inhabited.

Remark 7.1.2.

The number $n$ in Definition 7.1.1 (http://planetmath.org/71definitionofntypes#Thmpredefn1) ranges over all integers greater than or equal to $\mathrm{-}\mathrm{2}$. We could make sense of this formally by defining a type ${\mathrm{Z}}_{\mathrm{\ge }\mathrm{-}\mathrm{2}}$ of such integers (a type whose induction principle is identical to that of $\mathrm{N}$), or instead defining a predicate $\mathrm{is}\mathit{}\mathit{\text{-}}\mathit{}\mathrm{(}k\mathrm{-}\mathrm{2}\mathrm{)}\mathit{}\mathit{\text{-}}\mathit{}\mathrm{type}$ for $k\mathrm{:}\mathrm{N}$. Either way, we can prove theorems about $n$-types by induction on $n$, with $n\mathrm{=}\mathrm{-}\mathrm{2}$ as the base case.

Example 7.1.3.

We saw in Lemma 3.11.10 (http://planetmath.org/311contractibility#Thmprelem7) that $X$ is a $\mathrm{(}\mathrm{-}\mathrm{1}\mathrm{)}$-type if and only if it is a mere proposition. Therefore, $X$ is a $\mathrm{0}$-type if and only if it is a set.

We have also seen that there are types which are not sets (Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6)). So far, however, we have not shown for any $n>0$ that there exist types which are not $n$-types. In http://planetmath.org/node/87582Chapter 8, however, we will show that the $(n+1)$-sphere ${𝕊}^{n+1}$ is not an $n$-type. (Kraus has also shown that the $n^{\mathrm{th}}$ nested univalent universe is also not an $n$-type, without using any higher inductive types.) Moreover, in §8.8 (http://planetmath.org/88whiteheadstheoremandwhiteheadsprinciple) will give an example of a type that is not an $n$-type for any (finite) number $n$.

We begin the general theory of $n$-types by showing they are closed under certain operations and constructors.

Theorem 7.1.4.

Let $p\mathrm{:}X\mathrm{\to }Y$ be a retraction and suppose that $X$ is an $n$-type, for any $n\mathrm{\ge }\mathrm{-}\mathrm{2}$. Then $Y$ is also an $n$-type.

Proof.

We proceed by induction on $n$. The base case $n=-2$ is handled by Lemma 3.11.7 (http://planetmath.org/311contractibility#Thmprelem4).

For the inductive step, assume that any retract of an $n$-type is an $n$-type, and that $X$ is an $(n+1)$-type. Let $y,y^{\prime }:Y$; we must show that $y=y^{\prime }$ is an $n$-type. Let $s$ be a section of $p$, and let $ϵ$ be a homotopy $ϵ:p\circ s\sim 1$. Since $X$ is an $(n+1)$-type, $s(y){=}_{X}s(y^{\prime })$ is an $n$-type. We claim that $y=y^{\prime }$ is a retract of $s(y){=}_{X}s(y^{\prime })$. For the section, we take

$${\mathrm{𝖺𝗉}}_s:(y=y^{\prime })\to (s(y)=s(y^{\prime })).$$

For the retraction, we define $t:(s(y)=s(y^{\prime }))\to (y=y^{\prime })$ by

$$t(q):\equiv ϵ_y{}^{-1}p\left(q\right){ϵ}_{y^{\prime }}.$$

To show that $t$ is a retraction of ${\mathrm{𝖺𝗉}}_s$, we must show that

$$ϵ_y{}^{-1}p\left(s\left(r\right)\right){ϵ}_{y^{\prime }}=r$$

for any $r:y=y^{\prime }$. But this follows from Lemma 2.4.3 (http://planetmath.org/24homotopiesandequivalences#Thmprelem2). ∎

As an immediate corollary we obtain the stability of $n$-types under equivalence (which is also immediate from univalence):

Corollary 7.1.5.

If $X\mathrm{\simeq }Y$ and $X$ is an $n$-type, then so is $Y$.

Recall also the notion of embedding from §4.6 (http://planetmath.org/46surjectionsandembeddings).

Theorem 7.1.6.

If $f\mathrm{:}X\mathrm{\to }Y$ is an embedding and $Y$ is an $n$-type for some $n\mathrm{\ge }\mathrm{-}\mathrm{1}$, then so is $X$.

Proof.

Let $x,x^{\prime }:X$; we must show that $x{=}_X{x}^{\prime }$ is an $(n-1)$-type. But since $f$ is an embedding, we have $(x{=}_X{x}^{\prime })\simeq (f(x){=}_{Y}f(x^{\prime }))$, and the latter is an $(n-1)$-type by assumption. ∎

Note that this theorem fails when $n=-2$: the map $\mathrm{𝟎}\to \mathrm{𝟏}$ is an embedding, but $\mathrm{𝟏}$ is a $(-2)$-type while $\mathrm{𝟎}$ is not.

Theorem 7.1.7.

The hierarchy of $n$-types is cumulative in the following sense: given a number $n\mathrm{\ge }\mathrm{-}\mathrm{2}$, if $X$ is an $n$-type, then it is also an $\mathrm{(}n\mathrm{+}\mathrm{1}\mathrm{)}$-type.

Proof.

We proceed by induction on $n$.

For $n=-2$, we need to show that a contractible type, say, $A$, has contractible path spaces. Let $a_0:A$ be the center of contraction of $A$, and let $x,y:A$. We show that $x{=}_{A}y$ is contractible. By contractibility of $A$ we have a path ${\mathrm{𝖼𝗈𝗇𝗍𝗋}}_x\mathrm{𝖼𝗈𝗇𝗍𝗋}_y{}^{-1}:x=y$, which we choose as the center of contraction for $x=y$. Given any $p:x=y$, we need to show $p={\mathrm{𝖼𝗈𝗇𝗍𝗋}}_x\mathrm{𝖼𝗈𝗇𝗍𝗋}_y{}^{-1}$. By path induction, it suffices to show that ${\mathrm{𝗋𝖾𝖿𝗅}}_x={\mathrm{𝖼𝗈𝗇𝗍𝗋}}_x\mathrm{𝖼𝗈𝗇𝗍𝗋}_x{}^{-1}$, which is trivial.

For the inductive step, we need to show that $x{=}_{X}y$ is an $(n+1)$-type, provided that $X$ is an $(n+1)$-type. Applying the inductive hypothesis to $x{=}_{X}y$ yields the desired result. ∎

We now show that $n$-types are preserved by most of the type forming operations.

Theorem 7.1.8.

Let $n\mathrm{\ge }\mathrm{-}\mathrm{2}$, and let $A\mathrm{:}\mathrm{U}$ and $B\mathrm{:}A\mathrm{\to }\mathrm{U}$. If $A$ is an $n$-type and for all $a\mathrm{:}A$, $B\mathit{}\mathrm{(}a\mathrm{)}$ is an $n$-type, then so is ${\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}B\mathit{}\mathrm{(}x\mathrm{)}$.

Proof.

We proceed by induction on $n$.

For $n=-2$, we choose the center of contraction for ${\sum }_{(x:A)}B(x)$ to be the pair $(a_0,b_0)$, where $a_0:A$ is the center of contraction of $A$ and $b_0:B(a_0)$ is the center of contraction of $B(a_0)$. Given any other element $(a,b)$ of ${\sum }_{(x:A)}B(x)$, we provide a path $(a,b)=(a_0,b_0)$ by contractibility of $A$ and $B(a_0)$, respectively.

For the inductive step, suppose that $A$ is an $(n+1)$-type and for any $a:A$, $B(a)$ is an $(n+1)$-type. We show that ${\sum }_{(x:A)}B(x)$ is an $(n+1)$-type: fix $(a_1,b_1)$ and $(a_2,b_2)$ in ${\sum }_{(x:A)}B(x)$, we show that $(a_1,b_1)=(a_2,b_2)$ is an $n$-type. By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) we have

$$((a_1,b_1)=(a_2,b_2))\simeq \sum _{p:a_1=a_2}(p_{*}\left(b_1\right){=}_{B(a_2)}{b}_2)$$

and by preservation of $n$-types under equivalences (Corollary 7.1.5 (http://planetmath.org/71definitionofntypes#Thmprecor1)) it suffices to prove that the latter is an $n$-type. This follows from the inductive hypothesis. ∎

As a special case, if $A$ and $B$ are $n$-types, so is $A\times B$. Note also that Theorem 7.1.7 (http://planetmath.org/71definitionofntypes#Thmprethm3) implies that if $A$ is an $n$-type, then so is $x{=}_{A}y$ for any $x,y:A$. Combining this with Theorem 7.1.8 (http://planetmath.org/71definitionofntypes#Thmprethm4), we see that for any functions $f:A\to C$ and $g:B\to C$ between $n$-types, their pullback

$$A{\times }_{C}B:\equiv \sum _{(x:A)}\sum _{(y:B)}(f(x)=g(y))$$

(see http://planetmath.org/node/87642Exercise 2.11) is also an $n$-type. More generally, $n$-types are closed under all limits.

Theorem 7.1.9.

Let $n\mathrm{\ge }\mathrm{-}\mathrm{2}$, and let $A\mathrm{:}\mathrm{U}$ and $B\mathrm{:}A\mathrm{\to }\mathrm{U}$. If for all $a\mathrm{:}A$, $B\mathit{}\mathrm{(}a\mathrm{)}$ is an $n$-type, then so is ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}B\mathit{}\mathrm{(}x\mathrm{)}$.

Proof.

We proceed by induction on $n$. For $n=-2$, the result is simply Lemma 3.11.6 (http://planetmath.org/311contractibility#Thmprelem3).

For the inductive step, assume the result is true for $n$-types, and that each $B(a)$ is an $(n+1)$-type. Let $f,g:{\prod }_{(a:A)}B(a)$. We need to show that $f=g$ is an $n$-type. By function extensionality and closure of $n$-types under equivalence, it suffices to show that ${\prod }_{(a:A)}(f(a){=}_{B(a)}g(a))$ is an $n$-type. This follows from the inductive hypothesis. ∎

As a special case of the above theorem, the function space $A\to B$ is an $n$-type provided that $B$ is an $n$-type. We can now generalize our observations in http://planetmath.org/node/87569Chapter 2 that $\mathrm{𝗂𝗌𝖲𝖾𝗍}(A)$ and $\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(A)$ are mere propositions.

Theorem 7.1.10.

For any $n\mathrm{\ge }\mathrm{-}\mathrm{2}$ and any type $X$, the type $\mathrm{is}\mathit{}\mathit{\text{-}}\mathit{}n\mathit{}\mathit{\text{-}}\mathit{}\mathrm{type}\mathit{}\mathrm{(}X\mathrm{)}$ is a mere proposition.

Proof.

We proceed by induction with respect to $n$.

For the base case, we need to show that for any $X$, the type $\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(X)$ is a mere proposition. This is Lemma 3.11.4 (http://planetmath.org/311contractibility#Thmprelem2).

For the inductive step we need to show

$$\prod _{X:𝒰}\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(\mathrm{𝗂𝗌}\text{-}n\text{-}\mathrm{𝗍𝗒𝗉𝖾}(X))\to \prod _{X:𝒰}\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(\mathrm{𝗂𝗌}\text{-}(n+1)\text{-}\mathrm{𝗍𝗒𝗉𝖾}(X))$$

To show the conclusion of this implication, we need to show that for any type $X$, the type

$$\prod _{x,x^{\prime }:X}\mathrm{𝗂𝗌}\text{-}n\text{-}\mathrm{𝗍𝗒𝗉𝖾}(x=x^{\prime })$$

is a mere proposition. By Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2) or Theorem 7.1.9 (http://planetmath.org/71definitionofntypes#Thmprethm5), it suffices to show that for any $x,x^{\prime }:X$, the type $\mathrm{𝗂𝗌}\text{-}n\text{-}\mathrm{𝗍𝗒𝗉𝖾}(x{=}_X{x}^{\prime })$ is a mere proposition. But this follows from the inductive hypothesis applied to the type $(x{=}_X{x}^{\prime })$. ∎

Finally, we show that the type of $n$-types is itself an $(n+1)$-type. We define this to be:

$$n\text{-}\mathrm{𝖳𝗒𝗉𝖾}:\equiv \sum _{X:𝒰}\mathrm{𝗂𝗌}\text{-}n\text{-}\mathrm{𝗍𝗒𝗉𝖾}(X)$$

If necessary, we may specify the universe $𝒰$ by writing $n\text{-}{\mathrm{𝖳𝗒𝗉𝖾}}_{𝒰}$. In particular, we have $\mathrm{𝖯𝗋𝗈𝗉}:\equiv (-1)\text{-}\mathrm{𝖳𝗒𝗉𝖾}$ and $\mathrm{𝖲𝖾𝗍}:\equiv 0\text{-}\mathrm{𝖳𝗒𝗉𝖾}$, as defined in http://planetmath.org/node/87569Chapter 2. Note that just as for $\mathrm{𝖯𝗋𝗈𝗉}$ and $\mathrm{𝖲𝖾𝗍}$, because $\mathrm{𝗂𝗌}\text{-}n\text{-}\mathrm{𝗍𝗒𝗉𝖾}(X)$ is a mere proposition, by Lemma 3.5.1 (http://planetmath.org/35subsetsandpropositionalresizing#Thmprelem1) for any $(X,p),(X^{\prime },p^{\prime }):n\text{-}\mathrm{𝖳𝗒𝗉𝖾}$ we have

$\left((X,p){=}_{n\text{-}\mathrm{𝖳𝗒𝗉𝖾}}(X^{\prime },p^{\prime })\right)$ $\simeq (X{=}_{𝒰}{X}^{\prime })$

$\simeq (X\simeq X^{\prime }).$

Theorem 7.1.11.

For any $n\mathrm{\ge }\mathrm{-}\mathrm{2}$, the type $n\mathit{}\mathit{\text{-}}\mathit{}\mathrm{Type}$ is an $\mathrm{(}n\mathrm{+}\mathrm{1}\mathrm{)}$-type.

Proof.

Let $(X,p),(X^{\prime },p^{\prime }):n\text{-}\mathrm{𝖳𝗒𝗉𝖾}$; we need to show that $(X,p)=(X^{\prime },p^{\prime })$ is an $n$-type. By the above observation, this type is equivalent to $X\simeq X^{\prime }$. Next, we observe that the projection

$$(X\simeq X^{\prime })\to (X\to X^{\prime }).$$

is an embedding, so that if $n\ge -1$, then by Theorem 7.1.6 (http://planetmath.org/71definitionofntypes#Thmprethm2) it suffices to show that $X\to X^{\prime }$ is an $n$-type. But since $n$-types are preserved under the arrow type, this reduces to an assumption that $X^{\prime }$ is an $n$-type.

In the case $n=-2$, this argument shows that $X\simeq X^{\prime }$ is a $(-1)$-type — but it is also inhabited, since any two contractible types are equivalent to $\mathrm{𝟏}$, and hence to each other. Thus, $X\simeq X^{\prime }$ is also a $(-2)$-type. ∎

Title	7.1 Definition of n-types