7.3 Truncations

In §3.7 (http://planetmath.org/37propositionaltruncation) we introduced the propositional truncation, which makes the “best approximation” of a type that is a mere proposition, i.e. a $(-1)$-type. In §6.9 (http://planetmath.org/69truncations) we constructed this truncation as a higher inductive type, and gave one way to generalize it to a 0-truncation. We now explain a better generalization  of this, which truncates any type into an $n$-type for any $n\geq-2$; in classical homotopy theory this would be called its $n^{\mathrm{th}}$ Postnikov section.

The idea is to make use of (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem# utoref), which states that $A$ is an $n$-type just when $\Omega^{n+1}(A,a)$ is contractible  for all $a:A$, and Lemma 6.5.4 (http://planetmath.org/65suspensions#Thmprelem3), which implies that $\Omega^{n+1}(A,a)\simeq\mathsf{Map}_{*}(\mathbb{S}^{n+1},(A,a)),$ where $\mathbb{S}^{n+1}$ is equipped with some basepoint which we may as well call $\mathsf{base}$. However, contractibility of $\mathsf{Map}_{*}(\mathbb{S}^{n+1},(A,a))$ is something that we can ensure directly by giving path constructors.

We might first of all try to define $\mathopen{}\left\|A\right\|_{n}\mathclose{}$ to be generated by a function $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}:A\to\mathopen{}\left\|A% \right\|_{n}\mathclose{}$, together with for each $r:\mathbb{S}^{n+1}\to\mathopen{}\left\|A\right\|_{n}\mathclose{}$ and each $x:\mathbb{S}^{n+1}$, a path $s_{r}(x):r(x)=r(\mathsf{base})$. But this does not quite work, for the same reason that Remark 6.7.1 (http://planetmath.org/67hubsandspokes#Thmprermk1) fails. Instead, we use the full “hub and spoke” construction as in §6.7 (http://planetmath.org/67hubsandspokes).

Thus, for $n\geq-1$, we take $\mathopen{}\left\|A\right\|_{n}\mathclose{}$ to be the higher inductive type generated by:

• a function $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}:A\to\mathopen{}\left\|A% \right\|_{n}\mathclose{}$,

• for each $r:\mathbb{S}^{n+1}\to\mathopen{}\left\|A\right\|_{n}\mathclose{}$, a hub point $h(r):\mathopen{}\left\|A\right\|_{n}\mathclose{}$, and

• for each $r:\mathbb{S}^{n+1}\to\mathopen{}\left\|A\right\|_{n}\mathclose{}$ and each $x:\mathbb{S}^{n+1}$, a spoke path $s_{r}(x):r(x)=h(r)$.

The existence of these constructors is now enough to show:

Lemma 7.3.1.

$\mathopen{}\left\|A\right\|_{n}\mathclose{}$ is an $n$-type.

Proof.

By (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem# utoref), it suffices to show that $\Omega^{n+1}(\mathopen{}\left\|A\right\|_{n}\mathclose{},b)$ is contractible for all $b:\mathopen{}\left\|A\right\|_{n}\mathclose{}$, which by Lemma 6.5.4 (http://planetmath.org/65suspensions#Thmprelem3) is equivalent      to $\mathsf{Map}_{*}(\mathbb{S}^{n+1},(\mathopen{}\left\|A\right\|_{n}\mathclose{}% ,b)).$ As center of contraction for the latter, we choose the function $c_{b}:\mathbb{S}^{n+1}\to\mathopen{}\left\|A\right\|_{n}\mathclose{}$ which is constant at $b$, together with $\mathsf{refl}_{b}:c_{b}(\mathsf{base})=b$.

Now, an arbitrary element of $\mathsf{Map}_{*}(\mathbb{S}^{n+1},(\mathopen{}\left\|A\right\|_{n}\mathclose{}% ,b))$ consists of a map $r:\mathbb{S}^{n+1}\to\mathopen{}\left\|A\right\|_{n}\mathclose{}$ together with a path $p:r(\mathsf{base})=b$. By function extensionality, to show $r=c_{b}$ it suffices to give, for each $x:\mathbb{S}^{n+1}$, a path $r(x)=c_{b}(x)\equiv b$. We choose this to be the composite $s_{r}(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{{s_{r}(\mathsf{base})}^{-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$, where $s_{r}(x)$ is the spoke at $x$.

Finally, we must show that when transported along this equality $r=c_{b}$, the path $p$ becomes $\mathsf{refl}_{b}$. By transport in path types, this means we need

 $\mathord{{(s_{r}(\mathsf{base})\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{{s_{r}(\mathsf{base})}^% {-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)}^{-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=\mathsf{refl}_{b}.$

(This construction fails for $n=-2$, but in that case we can simply define $\mathopen{}\left\|A\right\|_{-2}\mathclose{}:\!\!\equiv\mathbf{1}$ for all $A$. From now on we assume $n\geq-1$.)

To show the desired universal property  of the $n$-truncation, we need the induction  principle. We extract this from the constructors in the usual way; it says that given $P:\mathopen{}\left\|A\right\|_{n}\mathclose{}\to\mathcal{U}$ together with

• For each $a:A$, an element $g(a):P(\mathopen{}\left|a\right|_{n}\mathclose{})$,

• For each $r:\mathbb{S}^{n+1}\to\mathopen{}\left\|A\right\|_{n}\mathclose{}$ and $r^{\prime}:\mathchoice{\prod_{x:\mathbb{S}^{n+1}}\,}{\mathchoice{{\textstyle% \prod_{(x:\mathbb{S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb% {S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})% }}{\prod_{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^% {n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(% x:\mathbb{S}^{n+1})}}}P(r(x))$, an element $h^{\prime}(r,r^{\prime}):P(h(r))$,

• For each $r:\mathbb{S}^{n+1}\to\mathopen{}\left\|A\right\|_{n}\mathclose{}$ and $r^{\prime}:\mathchoice{\prod_{x:\mathbb{S}^{n+1}}\,}{\mathchoice{{\textstyle% \prod_{(x:\mathbb{S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb% {S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})% }}{\prod_{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^% {n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(% x:\mathbb{S}^{n+1})}}}P(r(x))$, and each $x:\mathbb{S}^{n+1}$, a dependent path $r^{\prime}(x)=^{P}_{s_{r}(x)}h^{\prime}(r,r^{\prime})$,

there exists a section        $f:\mathchoice{\prod_{x:\mathopen{}\left\|A\right\|_{n}\mathclose{}}\,}{% \mathchoice{{\textstyle\prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}% }}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}{\prod_{(x:% \mathopen{}\left\|A\right\|_{n}\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A% \right\|_{n}\mathclose{})}}}{\mathchoice{{\textstyle\prod_{(x:\mathopen{}\left% \|A\right\|_{n}\mathclose{})}}}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}% \mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}{\prod% _{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}}{\mathchoice{{\textstyle% \prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}}{\prod_{(x:\mathopen{% }\left\|A\right\|_{n}\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}% \mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}}P(x)$ with $f(\mathopen{}\left|a\right|_{n}\mathclose{})\equiv g(a)$ for all $a:A$. To make this more useful, we reformulate it as follows.

Theorem 7.3.2.

For any type family $P:\mathopen{}\left\|A\right\|_{n}\mathclose{}\to\mathcal{U}$ such that each $P(x)$ is an $n$-type, and any function $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)}}}P(\mathopen{}\left|a\right% |_{n}\mathclose{})$, there exists a section $f:\mathchoice{\prod_{x:\mathopen{}\left\|A\right\|_{n}\mathclose{}}\,}{% \mathchoice{{\textstyle\prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}% }}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}{\prod_{(x:% \mathopen{}\left\|A\right\|_{n}\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A% \right\|_{n}\mathclose{})}}}{\mathchoice{{\textstyle\prod_{(x:\mathopen{}\left% \|A\right\|_{n}\mathclose{})}}}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}% \mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}{\prod% _{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}}{\mathchoice{{\textstyle% \prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}}{\prod_{(x:\mathopen{% }\left\|A\right\|_{n}\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}% \mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{n}\mathclose{})}}}P(x)$ such that $f(\mathopen{}\left|a\right|_{n}\mathclose{}):\!\!\equiv g(a)$ for all $a:A$.

Proof.

It will suffice to construct the second and third data listed above, since $g$ has exactly the type of the first datum. Given $r:\mathbb{S}^{n+1}\to\mathopen{}\left\|A\right\|_{n}\mathclose{}$ and $r^{\prime}:\mathchoice{\prod_{x:\mathbb{S}^{n+1}}\,}{\mathchoice{{\textstyle% \prod_{(x:\mathbb{S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb% {S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})% }}{\prod_{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^% {n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(% x:\mathbb{S}^{n+1})}}}P(r(x))$, we have $h(r):\mathopen{}\left\|A\right\|_{n}\mathclose{}$ and $s_{r}:\mathchoice{\prod_{x:\mathbb{S}^{n+1}}\,}{\mathchoice{{\textstyle\prod_{% (x:\mathbb{S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+% 1})}}{\prod_{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{% S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod% _{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{n+1})}}% }{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:% \mathbb{S}^{n+1})}}}(r(x)=h(r))$. Define $t:\mathbb{S}^{n+1}\to P(h(r))$ by $t(x):\!\!\equiv{s_{r}(x)}_{*}\mathopen{}\left({r^{\prime}(x)}\right)\mathclose{}$. Then since $P(h(r))$ is $n$-truncated, there exists a point $u:P(h(r))$ and a contraction $v:\mathchoice{\prod_{x:\mathbb{S}^{n+1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})% }}{\prod_{(x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^% {n+1})}}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(% x:\mathbb{S}^{n+1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{n+1})}}}{% \prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{S}^{n+1})}}{\prod_{(x:\mathbb{% S}^{n+1})}}}(t(x)=u)$. Define $h^{\prime}(r,r^{\prime}):\!\!\equiv u$, giving the second datum. Then (recalling the definition of dependent paths), $v$ has exactly the type required of the third datum. ∎

In particular, if $E$ is some $n$-type, we can consider the constant family of types equal to $E$ for every point of $A$. Thus, every map $f:A\to{}E$ can be extended to a map $\mathsf{ext}(f):\mathopen{}\left\|A\right\|_{n}\mathclose{}\to{}E$ defined by $\mathsf{ext}(f)(\mathopen{}\left|a\right|_{n}\mathclose{}):\!\!\equiv f(a)$; this is the recursion principle for $\mathopen{}\left\|A\right\|_{n}\mathclose{}$.

The induction principle also implies a uniqueness principle for functions of this form. Namely, if $E$ is an $n$-type and $g,g^{\prime}:\mathopen{}\left\|A\right\|_{n}\mathclose{}\to{}E$ are such that $g(\mathopen{}\left|a\right|_{n}\mathclose{})=g^{\prime}(\mathopen{}\left|a% \right|_{n}\mathclose{})$ for every $a:A$, then $g(x)=g^{\prime}(x)$ for all $x:\mathopen{}\left\|A\right\|_{n}\mathclose{}$, since the type $g(x)=g^{\prime}(x)$ is an $n$-type. Thus, $g=g^{\prime}$. This yields the following universal property.

Lemma 7.3.3 (Universal property of truncations).

Let $n\geq-2$, $A:\mathcal{U}$ and $B:{n}\text{-}\mathsf{Type}$. The following map is an equivalence:

 $\left\{\begin{array}[]{rcl}(\mathopen{}\left\|A\right\|_{n}\mathclose{}\to{}B)% &\longrightarrow&(A\to{}B)\\ g&\longmapsto&g\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}\end{% array}\right.$
Proof.

Given that $B$ is $n$-truncated, any $f:A\to{}B$ can be extended to a map $\mathsf{ext}(f):\mathopen{}\left\|A\right\|_{n}\mathclose{}\to{}B$. The map $\mathsf{ext}(f)\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}$ is equal to $f$, because for every $a:A$ we have $\mathsf{ext}(f)(\mathopen{}\left|a\right|_{n}\mathclose{})=f(a)$ by definition. And the map $\mathsf{ext}(g\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n})$ is equal to $g$, because they both send $\mathopen{}\left|a\right|_{n}\mathclose{}$ to $g(\mathopen{}\left|a\right|_{n}\mathclose{})$. ∎

In categorical  language  , this says that the $n$-types form a reflective subcategory of the category  of types. (To state this fully precisely, one ought to use the language of $(\infty,1)$-categories.) In particular, this implies that the $n$-truncation is functorial: given $f:A\to B$, applying the recursion principle to the composite $A\xrightarrow{f}B\to\mathopen{}\left\|B\right\|_{n}\mathclose{}$ yields a map $\mathopen{}\left\|f\right\|_{n}\mathclose{}:\mathopen{}\left\|A\right\|_{n}% \mathclose{}\to\mathopen{}\left\|B\right\|_{n}\mathclose{}$. By definition, we have a homotopy  $\mathsf{nat}^{f}_{n}:\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)}}}% \mathopen{}\left\|f\right\|_{n}\mathclose{}(\mathopen{}\left|a\right|_{n}% \mathclose{})=\mathopen{}\left|f(a)\right|_{n}\mathclose{},$ (7.3.4)

expressing naturality of the maps $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}$.

Uniqueness implies functoriality laws such as $\mathopen{}\left\|g\circ f\right\|_{n}\mathclose{}=\mathopen{}\left\|g\right\|% _{n}\mathclose{}\circ\mathopen{}\left\|f\right\|_{n}\mathclose{}$ and $\mathopen{}\left\|\mathsf{id}_{A}\right\|_{n}\mathclose{}=\mathsf{id}_{% \mathopen{}\left\|A\right\|_{n}\mathclose{}}$, with attendant coherence laws. We also have higher functoriality, for instance:

Lemma 7.3.5.

Given $f,g:A\to B$ and a homotopy $h:f\sim g$, there is an induced homotopy $\mathopen{}\left\|h\right\|_{n}\mathclose{}:\mathopen{}\left\|f\right\|_{n}% \mathclose{}\sim\mathopen{}\left\|g\right\|_{n}\mathclose{}$ such that the composite

 $\includegraphics{HoTT_{f}ig_{7}.3.1.png}$ (7.3.5)

is equal to $\mathsf{ap}_{|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}}(h(a))$.

Proof.

First, we indeed have a homotopy with components $\mathsf{ap}_{|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}}(h(a)):% \mathopen{}\left|f(a)\right|_{n}\mathclose{}=\mathopen{}\left|g(a)\right|_{n}% \mathclose{}$. Composing on either sides with the paths $\mathopen{}\left|f(a)\right|_{n}\mathclose{}=\mathopen{}\left\|f\right\|_{n}% \mathclose{}(\mathopen{}\left|a\right|_{n}\mathclose{})$ and $\mathopen{}\left|g(a)\right|_{n}\mathclose{}=\mathopen{}\left\|g\right\|_{n}% \mathclose{}(\mathopen{}\left|a\right|_{n}\mathclose{})$, which arise from the definitions of $\mathopen{}\left\|f\right\|_{n}\mathclose{}$ and $\mathopen{}\left\|g\right\|_{n}\mathclose{}$, we obtain a homotopy $(\mathopen{}\left\|f\right\|_{n}\mathclose{}\circ|\mathord{\hskip 1.0pt\text{-% -}\hskip 1.0pt}|_{n})\sim(\mathopen{}\left\|g\right\|_{n}\mathclose{}\circ|% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n})$, and hence an equality by function extensionality. But since $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ|\mathord{\hskip 1.0pt\text{-% -}\hskip 1.0pt}|_{n})$ is an equivalence, there must be a path $\mathopen{}\left\|f\right\|_{n}\mathclose{}=\mathopen{}\left\|g\right\|_{n}% \mathclose{}$ inducing it, and the coherence laws for function extensionality imply (7.3.5). ∎

The following observation about reflective subcategories is also standard.

Corollary 7.3.7.

A type $A$ is an $n$-type if and only if $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}:A\to\mathopen{}\left\|A% \right\|_{n}\mathclose{}$ is an equivalence.

Proof.

“If” follows from closure   of $n$-types under equivalence. On the other hand, if $A$ is an $n$-type, we can define $\mathsf{ext}(\mathsf{id}_{A}):\mathopen{}\left\|A\right\|_{n}\mathclose{}\to{}A$. Then we have $\mathsf{ext}(\mathsf{id}_{A})\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}% |_{n}=\mathsf{id}_{A}:A\to{}A$ by definition. In order to prove that $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}\circ\mathsf{ext}(\mathsf{id}% _{A})=\mathsf{id}_{\mathopen{}\left\|A\right\|_{n}\mathclose{}}$, we only need to prove that $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}\circ\mathsf{ext}(\mathsf{id}% _{A})\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}=\mathsf{id}_{% \mathopen{}\left\|A\right\|_{n}\mathclose{}}\circ|\mathord{\hskip 1.0pt\text{-% -}\hskip 1.0pt}|_{n}$. This is again true:

The category of $n$-types also has some special properties not possessed by all reflective subcategories. For instance, the reflector $\mathopen{}\left\|-\right\|_{n}\mathclose{}$ preserves finite products    .

Theorem 7.3.8.

For any types $A$ and $B$, the induced map $\mathopen{}\left\|A\times B\right\|_{n}\mathclose{}\to\mathopen{}\left\|A% \right\|_{n}\mathclose{}\times\mathopen{}\left\|B\right\|_{n}\mathclose{}$ is an equivalence.

Proof.

It suffices to show that $\mathopen{}\left\|A\right\|_{n}\mathclose{}\times\mathopen{}\left\|B\right\|_{% n}\mathclose{}$ has the same universal property as $\mathopen{}\left\|A\times B\right\|_{n}\mathclose{}$. Thus, let $C$ be an $n$-type; we have

 $\displaystyle(\mathopen{}\left\|A\right\|_{n}\mathclose{}\times\mathopen{}% \left\|B\right\|_{n}\mathclose{}\to C)$ $\displaystyle=(\mathopen{}\left\|A\right\|_{n}\mathclose{}\to(\mathopen{}\left% \|B\right\|_{n}\mathclose{}\to C))$ $\displaystyle=(\mathopen{}\left\|A\right\|_{n}\mathclose{}\to(B\to C))$ $\displaystyle=(A\to(B\to C))$ $\displaystyle=(A\times B\to C)$

using the universal properties of $\mathopen{}\left\|B\right\|_{n}\mathclose{}$ and $\mathopen{}\left\|A\right\|_{n}\mathclose{}$, along with the fact that $B\to C$ is an $n$-type since $C$ is. It is straightforward to verify that this equivalence is given by composing with $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}\times|\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}|_{n}$, as needed. ∎

The following related fact about dependent sums is often useful.

Theorem 7.3.9.

Let $P:A\to\mathcal{U}$ be a family of types. Then there is an equivalence

 $\Bigl{\|}\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)}}}\mathopen{}\left\|P(x)\right\|_{n% }\mathclose{}\Bigr{\|}_{n}\simeq\Bigl{\|}\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)}}}P(x)\Bigr{\|}_{n}.$
Proof.

We use the induction principle of $n$-truncation several times to construct functions

 $\displaystyle\varphi$ $\displaystyle:\Bigl{\|}\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)}}}\mathopen{}% \left\|P(x)\right\|_{n}\mathclose{}\Bigr{\|}_{n}\to\Bigl{\|}\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)}}}P(x)\Bigr{\|}_{n}$ $\displaystyle\psi$ $\displaystyle:\Bigl{\|}\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)}}}P(x)\Bigr{% \|}_{n}\to\Bigl{\|}\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)}}}\mathopen{}\left\|P(x)% \right\|_{n}\mathclose{}\Bigr{\|}_{n}$

and homotopies $H:\varphi\circ\psi\sim\mathsf{id}$ and $K:\psi\circ\varphi\sim\mathsf{id}$ exhibiting them as quasi-inverses. We define $\varphi$ by setting $\varphi(\mathopen{}\left|{\mathopen{}(x,\mathopen{}\left|u\right|_{n}% \mathclose{})\mathclose{}}\right|_{n}\mathclose{}):\!\!\equiv\mathopen{}\left|% {\mathopen{}(x,u)\mathclose{}}\right|_{n}\mathclose{}$. We define $\psi$ by setting $\psi(\mathopen{}\left|{\mathopen{}(x,u)\mathclose{}}\right|_{n}\mathclose{}):% \!\!\equiv\mathopen{}\left|{\mathopen{}(x,\mathopen{}\left|u\right|_{n}% \mathclose{})\mathclose{}}\right|_{n}\mathclose{}$. Then we define $H(\mathopen{}\left|{\mathopen{}(x,u)\mathclose{}}\right|_{n}\mathclose{}):\!\!% \equiv\mathsf{refl}_{\mathopen{}\left|{\mathopen{}(x,u)\mathclose{}}\right|_{n% }\mathclose{}}$ and $K(\mathopen{}\left|{\mathopen{}(x,\mathopen{}\left|u\right|_{n}\mathclose{})% \mathclose{}}\right|_{n}\mathclose{}):\!\!\equiv\mathsf{refl}_{\mathopen{}% \left|{\mathopen{}(x,\mathopen{}\left|u\right|_{n}\mathclose{})\mathclose{}}% \right|_{n}\mathclose{}}$. ∎

Corollary 7.3.10.

If $A$ is an $n$-type and $P:A\to\mathcal{U}$ is any type family, then

 $\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{% \sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)% }}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a% :A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathopen{}\left\|P(a)\right\|_{n}\mathclose% {}\simeq\Bigl{\|}\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}% }}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:% A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{% (a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}P(a)\Bigr{\|}_{n}$
Proof.

If $A$ is an $n$-type, then the left-hand type above is already an $n$-type, hence equivalent to its $n$-truncation; thus this follows from Theorem 7.3.9 (http://planetmath.org/73truncations#Thmprethm3). ∎

We can characterize the path spaces of a truncation using the same method that we used in §2.12 (http://planetmath.org/212coproducts),§2.13 (http://planetmath.org/213naturalnumbers) for coproducts  and natural numbers  (and which we will use in http://planetmath.org/node/87582Chapter 8 to calculate homotopy groups  ). Unsurprisingly, the path spaces in the $(n+1)$-truncation of $A$ are the $n$-truncations of the path spaces of $A$. Indeed, for any $x,y:A$ there is a canonical map

 $f:\bigl{\|}x=_{A}y\bigr{\|}_{n}\to\Big{(}\mathopen{}\left|x\right|_{n+1}% \mathclose{}=_{\mathopen{}\left\|A\right\|_{n+1}\mathclose{}}\mathopen{}\left|% y\right|_{n+1}\mathclose{}\Big{)}$ (7.3.11)

defined by

 $f(\mathopen{}\left|p\right|_{n}\mathclose{}):\!\!\equiv\mathsf{ap}_{|\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}|_{n+1}}(p).$

This definition uses the recursion principle for $\|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\|_{n}$, which is correct because $\mathopen{}\left\|A\right\|_{n+1}\mathclose{}$ is $(n+1)$-truncated, so that the codomain of $f$ is $n$-truncated.

Theorem 7.3.12.

For any $A$ and $x,y:A$ and $n\geq-2$, the map (7.3.11) is an equivalence; thus we have

 $\bigl{\|}x=_{A}y\bigr{\|}_{n}\simeq\Big{(}\mathopen{}\left|x\right|_{n+1}% \mathclose{}=_{\mathopen{}\left\|A\right\|_{n+1}\mathclose{}}\mathopen{}\left|% y\right|_{n+1}\mathclose{}\Big{)}.$
Proof.

The proof is a simple application of the encode-decode method: As in previous situations, we cannot directly define a quasi-inverse to the map (7.3.11) because there is no way to induct on an equality between $\mathopen{}\left|x\right|_{n+1}\mathclose{}$ and $\mathopen{}\left|y\right|_{n+1}\mathclose{}$. Thus, instead we generalize its type, in order to have general elements of the type $\mathopen{}\left\|A\right\|_{n+1}\mathclose{}$ instead of $\mathopen{}\left|x\right|_{n+1}\mathclose{}$ and $\mathopen{}\left|y\right|_{n+1}\mathclose{}$. Define $P:\mathopen{}\left\|A\right\|_{n+1}\mathclose{}\to\mathopen{}\left\|A\right\|_% {n+1}\mathclose{}\to{n}\text{-}\mathsf{Type}$ by

 $P(\mathopen{}\left|x\right|_{n+1}\mathclose{},\mathopen{}\left|y\right|_{n+1}% \mathclose{}):\!\!\equiv\mathopen{}\left\|x=_{A}y\right\|_{n}\mathclose{}$

This definition is correct because $\mathopen{}\left\|x=_{A}y\right\|_{n}\mathclose{}$ is $n$-truncated, and ${n}\text{-}\mathsf{Type}$ is $(n+1)$-truncated by Theorem 7.1.11 (http://planetmath.org/71definitionofntypes#Thmprethm7). Now for every $u,v:\mathopen{}\left\|A\right\|_{n+1}\mathclose{}$, there is a map

 $\mathsf{encode}:P(u,v)\to\big{(}u=_{\mathopen{}\left\|A\right\|_{n+1}% \mathclose{}}v\big{)}$

defined for $u=\mathopen{}\left|x\right|_{n+1}\mathclose{}$ and $v=\mathopen{}\left|y\right|_{n+1}\mathclose{}$ and $p:x=y$ by

 $\mathsf{encode}(\mathopen{}\left|p\right|_{n}\mathclose{}):\!\!\equiv\mathsf{% ap}_{\mathopen{}\left|\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0% pt}\right|_{n+1}\mathclose{}}(p).$

Since the codomain of $\mathsf{encode}$ is $n$-truncated, it suffices to define it only for $u$ and $v$ of this form, and then it’s just the same definition as before. We also define a function

 $r:\mathchoice{\prod_{u:\mathopen{}\left\|A\right\|_{n+1}\mathclose{}}\,}{% \mathchoice{{\textstyle\prod_{(u:\mathopen{}\left\|A\right\|_{n+1}\mathclose{}% )}}}{\prod_{(u:\mathopen{}\left\|A\right\|_{n+1}\mathclose{})}}{\prod_{(u:% \mathopen{}\left\|A\right\|_{n+1}\mathclose{})}}{\prod_{(u:\mathopen{}\left\|A% \right\|_{n+1}\mathclose{})}}}{\mathchoice{{\textstyle\prod_{(u:\mathopen{}% \left\|A\right\|_{n+1}\mathclose{})}}}{\prod_{(u:\mathopen{}\left\|A\right\|_{% n+1}\mathclose{})}}{\prod_{(u:\mathopen{}\left\|A\right\|_{n+1}\mathclose{})}}% {\prod_{(u:\mathopen{}\left\|A\right\|_{n+1}\mathclose{})}}}{\mathchoice{{% \textstyle\prod_{(u:\mathopen{}\left\|A\right\|_{n+1}\mathclose{})}}}{\prod_{(% u:\mathopen{}\left\|A\right\|_{n+1}\mathclose{})}}{\prod_{(u:\mathopen{}\left% \|A\right\|_{n+1}\mathclose{})}}{\prod_{(u:\mathopen{}\left\|A\right\|_{n+1}% \mathclose{})}}}P(u,u)$

by induction on $u$, where $r(\mathopen{}\left|x\right|_{n+1}\mathclose{}):\!\!\equiv\mathopen{}\left|% \mathsf{refl}_{x}\right|_{n}\mathclose{}$.

Now we can define an inverse map

 $\mathsf{decode}:(u=_{\mathopen{}\left\|A\right\|_{n+1}\mathclose{}}v)\to P(u,v)$

by

 $\mathsf{decode}(p):\!\!\equiv\mathsf{transport}^{v\mapsto P(u,v)}(p,r(u)).$

To show that the composite

 $(u=_{\mathopen{}\left\|A\right\|_{n+1}\mathclose{}}v)\xrightarrow{\mathsf{% decode}}P(u,v)\xrightarrow{\mathsf{encode}}(u=_{\mathopen{}\left\|A\right\|_{n% +1}\mathclose{}}v)$

is the identity function, by path induction it suffices to check it for $\mathsf{refl}_{u}:u=u$, in which case what we need to know is that $\mathsf{decode}(r(u))=\mathsf{refl}_{u}$. But since this is an $n$-type, hence also an $(n+1)$-type, we may assume $u\equiv\mathopen{}\left|x\right|_{n+1}\mathclose{}$, in which case it follows by definition of $r$ and $\mathsf{decode}$. Finally, to show that

 $P(u,v)\xrightarrow{\mathsf{encode}}(u=_{\mathopen{}\left\|A\right\|_{n+1}% \mathclose{}}v)\xrightarrow{\mathsf{decode}}P(u,v)$

is the identity function, since this goal is again an $n$-type, we may assume that $u=\mathopen{}\left|x\right|_{n+1}\mathclose{}$ and $v=\mathopen{}\left|y\right|_{n+1}\mathclose{}$ and that we are considering $\mathopen{}\left|p\right|_{n}\mathclose{}:P(\mathopen{}\left|x\right|_{n+1}% \mathclose{},\mathopen{}\left|y\right|_{n+1}\mathclose{})$ for some $p:x=y$. Then we have

 $\displaystyle\mathsf{decode}(\mathsf{encode}(\mathopen{}\left|p\right|_{n}% \mathclose{}))$ $\displaystyle=\mathsf{decode}(\mathsf{ap}_{\mathopen{}\left|\mathord{\hskip 1.% 0pt\underline{\hskip 4.3pt}\hskip 1.0pt}\right|_{n+1}\mathclose{}}(p))$ $\displaystyle=\mathsf{transport}^{v\mapsto P(\mathopen{}\left|x\right|_{n+1}% \mathclose{},v)}(\mathsf{ap}_{\mathopen{}\left|\mathord{\hskip 1.0pt\underline% {\hskip 4.3pt}\hskip 1.0pt}\right|_{n+1}\mathclose{}}(p),\mathopen{}\left|% \mathsf{refl}_{x}\right|_{n}\mathclose{})$ $\displaystyle=\mathsf{transport}^{v\mapsto\mathopen{}\left\|u=v\right\|_{n}% \mathclose{}}(p,\mathopen{}\left|\mathsf{refl}_{x}\right|_{n}\mathclose{})$ $\displaystyle=\mathopen{}\left|\mathsf{transport}^{v\mapsto(u=v)}(p,\mathsf{% refl}_{x})\right|_{n}\mathclose{}$ $\displaystyle=\mathopen{}\left|p\right|_{n}\mathclose{}.$

This completes      the proof that $\mathsf{encode}$ and $\mathsf{decode}$ are quasi-inverses. The stated result is then the special case where $u=\mathopen{}\left|x\right|_{n+1}\mathclose{}$ and $v=\mathopen{}\left|y\right|_{n+1}\mathclose{}$. ∎

Corollary 7.3.13.

Let $n\geq-2$ and $(A,a)$ be a pointed type. Then

 $\bigl{\|}\Omega(A,a)\bigr{\|}_{n}=\Omega\mathopen{}\left(\mathopen{}\left\|(A,% a)\right\|_{n+1}\mathclose{}\right)$
Proof.

This is a special case of the previous lemma where $x=y=a$. ∎

Corollary 7.3.14.

Let $n\geq-2$ and $k\geq 0$ and $(A,a)$ a pointed type. Then

 $\bigl{\|}\Omega^{k}(A,a)\bigr{\|}_{n}=\Omega^{k}\mathopen{}\left(\mathopen{}% \left\|(A,a)\right\|_{n+k}\mathclose{}\right).$
Proof.

By induction on $k$, using the recursive definition of $\Omega^{k}$. ∎

We also observe that “truncations are cumulative”: if we truncate to an $n$-type and then to a $k$-type with $k\leq n$, then we might as well have truncated directly to a $k$-type.

Lemma 7.3.15.

Let $k,n\geq-2$ with $k\leq{}n$ and $A:\mathcal{U}$. Then $\mathopen{}\left\|\mathopen{}\left\|A\right\|_{n}\mathclose{}\right\|_{k}% \mathclose{}=\mathopen{}\left\|A\right\|_{k}\mathclose{}$.

Proof.

We define two maps $f:\mathopen{}\left\|\mathopen{}\left\|A\right\|_{n}\mathclose{}\right\|_{k}% \mathclose{}\to\mathopen{}\left\|A\right\|_{k}\mathclose{}$ and $g:\mathopen{}\left\|A\right\|_{k}\mathclose{}\to\mathopen{}\left\|\mathopen{}% \left\|A\right\|_{n}\mathclose{}\right\|_{k}\mathclose{}$ by

 $f(\mathopen{}\left|\mathopen{}\left|a\right|_{n}\mathclose{}\right|_{k}% \mathclose{}):\!\!\equiv\mathopen{}\left|a\right|_{k}\mathclose{}\qquad\text{% and}\qquad g(\mathopen{}\left|a\right|_{k}\mathclose{}):\!\!\equiv\mathopen{}% \left|\mathopen{}\left|a\right|_{n}\mathclose{}\right|_{k}\mathclose{}.$

The map $f$ is well-defined because $\mathopen{}\left\|A\right\|_{k}\mathclose{}$ is $k$-truncated and also $n$-truncated (because $k\leq{}n$), and the map $g$ is well-defined because $\mathopen{}\left\|\mathopen{}\left\|A\right\|_{n}\mathclose{}\right\|_{k}% \mathclose{}$ is $k$-truncated.

The composition $f\circ{}g:\mathopen{}\left\|A\right\|_{k}\mathclose{}\to\mathopen{}\left\|A% \right\|_{k}\mathclose{}$ satisfies $(f\circ{}g)(\mathopen{}\left|a\right|_{k}\mathclose{})=\mathopen{}\left|a% \right|_{k}\mathclose{}$, hence $f\circ{}g=\mathsf{id}_{\mathopen{}\left\|A\right\|_{k}\mathclose{}}$. Similarly, we have $(g\circ{}f)(\mathopen{}\left|\mathopen{}\left|a\right|_{n}\mathclose{}\right|_% {k}\mathclose{})=\mathopen{}\left|\mathopen{}\left|a\right|_{n}\mathclose{}% \right|_{k}\mathclose{}$ and hence $g\circ{}f=\mathsf{id}_{\mathopen{}\left\|\mathopen{}\left\|A\right\|_{n}% \mathclose{}\right\|_{k}\mathclose{}}$. ∎

Title 7.3 Truncations
\metatable