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}.$

But this is immediate from path operations. ∎

(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:

\includegraphics

HoTT_fig_7.3.2.png

∎

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)$

$\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

	$\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)$

	$\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{}.$