# 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   $\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{type}:\mathcal{U}\to\mathcal{U}$ for $n\geq-2$ by recursion as follows:

 $\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{type}(X):\!\!\equiv\begin{cases}\mathsf{% isContr}(X)&\text{ if }n=-2,\\ \mathchoice{\prod_{x,y:X}\,}{\mathchoice{{\textstyle\prod_{(x,y:X)}}}{\prod_{(% x,y:X)}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}}{\mathchoice{{\textstyle\prod_{(x,y% :X)}}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}}{\mathchoice{{% \textstyle\prod_{(x,y:X)}}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}% }\mathsf{is}\mbox{-}{n^{\prime}}\mbox{-}\mathsf{type}(x=_{X}y)&\text{ if }n=n^% {\prime}+1.\end{cases}$

We say that $X$ is an $n$-type, or sometimes that it is $n$-truncated, if $\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{type}(X)$ 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 $-2$. We could make sense of this formally by defining a type $\mathbb{Z}_{{\geq}-2}$ of such integers (a type whose induction  principle is identical to that of $\mathbb{N}$), or instead defining a predicate $\mathsf{is}\mbox{-}{(k-2)}\mbox{-}\mathsf{type}$ for $k:\mathbb{N}$. Either way, we can prove theorems  about $n$-types by induction on $n$, with $n=-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 $(-1)$-type if and only if it is a mere proposition. Therefore, $X$ is a $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 $\mathbb{S}^{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:X\to Y$ be a retraction  and suppose that $X$ is an $n$-type, for any $n\geq-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 $\epsilon$ be a homotopy $\epsilon: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

 $\mathsf{ap}_{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\mathord{{\epsilon_{y}}^{-1}}\mathchoice{\mathbin{\raisebox{2.1% 5pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}{p}\mathopen{}\left({q}\right)% \mathclose{}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}% }{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\epsilon_{y^{\prime}}.$

To show that $t$ is a retraction of $\mathsf{ap}_{s}$, we must show that

 $\mathord{{\epsilon_{y}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}{p}\mathopen{}\left({{s}% \mathopen{}\left({r}\right)\mathclose{}}\right)\mathclose{}\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\epsilon_{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\simeq Y$ and $X$ is an $n$-type, then so is $Y$.

###### Theorem 7.1.6.

If $f:X\to Y$ is an embedding and $Y$ is an $n$-type for some $n\geq-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 $\mathbf{0}\to\mathbf{1}$ is an embedding, but $\mathbf{1}$ is a $(-2)$-type while $\mathbf{0}$ is not.

###### Theorem 7.1.7.

The hierarchy of $n$-types is cumulative in the following sense: given a number $n\geq-2$, if $X$ is an $n$-type, then it is also an $(n+1)$-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 $\mathsf{contr}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\mathord{{\mathsf{contr}_{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=\mathsf{contr}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\mathord{{\mathsf{contr}_{y}}^{-1}}$. By path induction, it suffices to show that $\mathsf{refl}_{x}=\mathsf{contr}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{\mathsf{contr}_{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\geq-2$, and let $A:\mathcal{U}$ and $B:A\to\mathcal{U}$. If $A$ is an $n$-type and for all $a:A$, $B(a)$ is an $n$-type, then so is $\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)$.

###### Proof.

We proceed by induction on $n$.

For $n=-2$, we choose the center of contraction for $\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)$ 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 $\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)$, 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 $\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 an $(n+1)$-type: fix $(a_{1},b_{1})$ and $(a_{2},b_{2})$ in $\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)$, 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\;\mathchoice{\sum_{p:a_{1}=a_{2}}\,}{% \mathchoice{{\textstyle\sum_{(p:a_{1}=a_{2})}}}{\sum_{(p:a_{1}=a_{2})}}{\sum_{% (p:a_{1}=a_{2})}}{\sum_{(p:a_{1}=a_{2})}}}{\mathchoice{{\textstyle\sum_{(p:a_{% 1}=a_{2})}}}{\sum_{(p:a_{1}=a_{2})}}{\sum_{(p:a_{1}=a_{2})}}{\sum_{(p:a_{1}=a_% {2})}}}{\mathchoice{{\textstyle\sum_{(p:a_{1}=a_{2})}}}{\sum_{(p:a_{1}=a_{2})}% }{\sum_{(p:a_{1}=a_{2})}}{\sum_{(p:a_{1}=a_{2})}}}({p}_{*}\mathopen{}\left({b_% {1}}\right)\mathclose{}=_{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\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)}}}\mathchoice% {\sum_{(y:B)}\,}{\mathchoice{{\textstyle\sum_{(y:B)}}}{\sum_{(y:B)}}{\sum_{(y:% B)}}{\sum_{(y:B)}}}{\mathchoice{{\textstyle\sum_{(y:B)}}}{\sum_{(y:B)}}{\sum_{% (y:B)}}{\sum_{(y:B)}}}{\mathchoice{{\textstyle\sum_{(y:B)}}}{\sum_{(y:B)}}{% \sum_{(y:B)}}{\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\geq-2$, and let $A:\mathcal{U}$ and $B:A\to\mathcal{U}$. If for all $a:A$, $B(a)$ is an $n$-type, then so is $\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)$.

###### 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:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\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 $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\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 $\mathsf{isSet}(A)$ and $\mathsf{isProp}(A)$ are mere propositions.

###### Theorem 7.1.10.

For any $n\geq-2$ and any type $X$, the type $\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{type}(X)$ 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 $\mathsf{isContr}(X)$ is a mere proposition. This is Lemma 3.11.4 (http://planetmath.org/311contractibility#Thmprelem2).

For the inductive step we need to show

 $\mathchoice{\prod_{X:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_{(X:\mathcal% {U})}}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:\mathcal{U% })}}}{\mathchoice{{\textstyle\prod_{(X:\mathcal{U})}}}{\prod_{(X:\mathcal{U})}% }{\prod_{(X:\mathcal{U})}}{\prod_{(X:\mathcal{U})}}}{\mathchoice{{\textstyle% \prod_{(X:\mathcal{U})}}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:\mathcal{U})}}{% \prod_{(X:\mathcal{U})}}}\mathsf{isProp}(\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf% {type}(X))\to\mathchoice{\prod_{X:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod% _{(X:\mathcal{U})}}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:\mathcal{U})}}{\prod_{% (X:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(X:\mathcal{U})}}}{\prod_{(X:% \mathcal{U})}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:\mathcal{U})}}}{\mathchoice{% {\textstyle\prod_{(X:\mathcal{U})}}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:% \mathcal{U})}}{\prod_{(X:\mathcal{U})}}}\mathsf{isProp}(\mathsf{is}\mbox{-}{(n% +1)}\mbox{-}\mathsf{type}(X))$

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

 $\mathchoice{\prod_{x,x^{\prime}:X}\,}{\mathchoice{{\textstyle\prod_{(x,x^{% \prime}:X)}}}{\prod_{(x,x^{\prime}:X)}}{\prod_{(x,x^{\prime}:X)}}{\prod_{(x,x^% {\prime}:X)}}}{\mathchoice{{\textstyle\prod_{(x,x^{\prime}:X)}}}{\prod_{(x,x^{% \prime}:X)}}{\prod_{(x,x^{\prime}:X)}}{\prod_{(x,x^{\prime}:X)}}}{\mathchoice{% {\textstyle\prod_{(x,x^{\prime}:X)}}}{\prod_{(x,x^{\prime}:X)}}{\prod_{(x,x^{% \prime}:X)}}{\prod_{(x,x^{\prime}:X)}}}\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{% type}(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 $\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{type}(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{-}\mathsf{Type}:\!\!\equiv\mathchoice{\sum_{X:\mathcal{U}}\,}{% \mathchoice{{\textstyle\sum_{(X:\mathcal{U})}}}{\sum_{(X:\mathcal{U})}}{\sum_{% (X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(X:% \mathcal{U})}}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(X:\mathcal{U})}}}{\sum_{(X:% \mathcal{U})}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}}\mathsf{is}% \mbox{-}{n}\mbox{-}\mathsf{type}(X)$

If necessary, we may specify the universe $\mathcal{U}$ by writing ${n}\text{-}\mathsf{Type}_{\mathcal{U}}$. In particular, we have $\mathsf{Prop}:\!\!\equiv{(-1)}\text{-}\mathsf{Type}$ and $\mathsf{Set}:\!\!\equiv{0}\text{-}\mathsf{Type}$, as defined in http://planetmath.org/node/87569Chapter 2. Note that just as for $\mathsf{Prop}$ and $\mathsf{Set}$, because $\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{type}(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{-}\mathsf{Type}$ we have

 $\displaystyle\Big{(}(X,p)=_{{n}\text{-}\mathsf{Type}}(X^{\prime},p^{\prime})% \Big{)}$ $\displaystyle\simeq(X=_{\mathcal{U}}X^{\prime})$ $\displaystyle\simeq(X\simeq X^{\prime}).$
###### Theorem 7.1.11.

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

###### Proof.

Let $(X,p),(X^{\prime},p^{\prime}):{n}\text{-}\mathsf{Type}$; 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\rightarrow X^{\prime}).$

is an embedding, so that if $n\geq-1$, then by Theorem 7.1.6 (http://planetmath.org/71definitionofntypes#Thmprethm2) it suffices to show that $X\rightarrow 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 $\mathbf{1}$, and hence to each other. Thus, $X\simeq X^{\prime}$ is also a $(-2)$-type. ∎

Title 7.1 Definition of n-types
\metatable