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 mereproposition, 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 a0-truncation.We now explain a better generalization of this, which truncates any type into an $n$-type for any $n\ge -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 ${\mathrm{\Omega }}^{n+1}(A,a)$is contractible forall $a:A$, and Lemma 6.5.4 (http://planetmath.org/65suspensions#Thmprelem3), which implies that${\mathrm{\Omega }}^{n+1}(A,a)\simeq {\mathrm{𝖬𝖺𝗉}}_{*}({𝕊}^{n+1},(A,a)),$ where ${𝕊}^{n+1}$ is equipped with some basepoint which we may as well call $\mathrm{𝖻𝖺𝗌𝖾}$.However, contractibility of ${\mathrm{𝖬𝖺𝗉}}_{*}({𝕊}^{n+1},(A,a))$ is something that we can ensure directly by giving path constructors.

We might first of all try to define ${\parallel A\parallel }_n$ to be generated by a function $|\text{–}{|}_n:A\to \parallel A{\parallel }_n$, together with for each$r:{𝕊}^{n+1}\to \parallel A{\parallel }_n$ and each $x:{𝕊}^{n+1}$, a path $s_r(x):r(x)=r(\mathrm{𝖻𝖺𝗌𝖾})$.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\ge -1$, we take ${\parallel A\parallel }_n$ to be the higher inductive type generated by:

• a function $|\text{–}{|}_n:A\to \parallel A{\parallel }_n$,

• for each $r:{𝕊}^{n+1}\to \parallel A{\parallel }_n$, a hub point $h(r):\parallel A{\parallel }_n$, and

• for each $r:{𝕊}^{n+1}\to \parallel A{\parallel }_n$ and each $x:{𝕊}^{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.

${\parallel A\parallel }_n$ is an $n$-type.

Proof.

By (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem# utoref), it suffices to show that ${\mathrm{\Omega }}^{n+1}(\parallel A{\parallel }_n,b)$ is contractible for all $b:\parallel A{\parallel }_n$, which byLemma 6.5.4 (http://planetmath.org/65suspensions#Thmprelem3) is equivalent to ${\mathrm{𝖬𝖺𝗉}}_{*}({𝕊}^{n+1},(\parallel A{\parallel }_n,b)).$As center of contraction for the latter, we choose the function $c_b:{𝕊}^{n+1}\to \parallel A{\parallel }_n$ which is constant at $b$, together with${\mathrm{𝗋𝖾𝖿𝗅}}_b:c_b(\mathrm{𝖻𝖺𝗌𝖾})=b$.

Now, an arbitrary element of ${\mathrm{𝖬𝖺𝗉}}_{*}({𝕊}^{n+1},(\parallel A{\parallel }_n,b))$ consists of a map $r:{𝕊}^{n+1}\to \parallel A{\parallel }_n$ together with a path$p:r(\mathrm{𝖻𝖺𝗌𝖾})=b$.By function extensionality, to show $r=c_b$ it suffices to give, for each $x:{𝕊}^{n+1}$, a path $r(x)=c_b(x)\equiv b$.We choose this to be the composite $s_r(x)s_r{(\mathrm{𝖻𝖺𝗌𝖾})}^{-1}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 ${\mathrm{𝗋𝖾𝖿𝗅}}_b$.By transport in path types, this means we need

$${(s_r(\mathrm{𝖻𝖺𝗌𝖾})s_r{(\mathrm{𝖻𝖺𝗌𝖾})}^{-1}p)}^{-1}p={\mathrm{𝗋𝖾𝖿𝗅}}_b.$$

But this is immediate from path operations.∎

(This construction fails for $n=-2$, but in that case we can simply define $\parallel A{\parallel }_{-2}:\equiv \mathrm{𝟏}$ for all $A$.From now on we assume $n\ge -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:\parallel A{\parallel }_n\to 𝒰$ together with

• For each $a:A$, an element $g(a):P(|a{|}_n)$,

• For each $r:{𝕊}^{n+1}\to \parallel A{\parallel }_n$ and $r^{\prime }:{\prod }_{(x:{𝕊}^{n+1})}P(r(x))$, an element $h^{\prime }(r,r^{\prime }):P(h(r))$,

• For each $r:{𝕊}^{n+1}\to \parallel A{\parallel }_n$ and $r^{\prime }:{\prod }_{(x:{𝕊}^{n+1})}P(r(x))$, and each $x:{𝕊}^{n+1}$, a dependent path$r^{\prime }(x){=}_{s_r(x)}^P{h}^{\prime }(r,r^{\prime })$,

there exists a section $f:{\prod }_{(x:\parallel A{\parallel }_n)}P(x)$ with $f(|a{|}_n)\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\mathrm{:}\mathrm{\parallel }A{\mathrm{\parallel }}_n\mathrm{\to }\mathrm{U}$ such that each $P\mathit{}\mathrm{(}x\mathrm{)}$ is an $n$-type, and any function $g\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}a\mathrm{:}A\mathrm{)}}P\mathrm{(}\mathrm{|}a{\mathrm{|}}_n\mathrm{)}$, thereexists a section $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}\mathrm{\parallel }A{\mathrm{\parallel }}_n\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$ such that $f\mathrm{(}\mathrm{|}a{\mathrm{|}}_n\mathrm{)}\mathrm{:}\mathrm{\equiv }g\mathrm{(}a\mathrm{)}$ for all $a\mathrm{:}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:{𝕊}^{n+1}\to \parallel A{\parallel }_n$ and $r^{\prime }:{\prod }_{(x:{𝕊}^{n+1})}P(r(x))$, we have $h(r):\parallel A{\parallel }_n$ and $s_r:{\prod }_{(x:{𝕊}^{n+1})}(r(x)=h(r))$.Define $t:{𝕊}^{n+1}\to P(h(r))$ by $t(x):\equiv s_r{(x)}_{*}\left(r^{\prime }(x)\right)$.Then since $P(h(r))$ is $n$-truncated, there exists a point $u:P(h(r))$ and a contraction $v:{\prod }_{(x:{𝕊}^{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 $\mathrm{𝖾𝗑𝗍}(f):\parallel A{\parallel }_n\to E$ defined by $\mathrm{𝖾𝗑𝗍}(f)(|a{|}_n):\equiv f(a)$; this is the recursion principle for ${\parallel A\parallel }_n$.

The induction principle also implies a uniqueness principle for functions of this form.Namely, if $E$ is an $n$-type and $g,g^{\prime }:\parallel A{\parallel }_n\to E$ are suchthat $g(|a{|}_n)=g^{\prime }(|a{|}_n)$ for every $a:A$, then $g(x)=g^{\prime }(x)$ for all $x:\parallel A{\parallel }_n$, 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\mathrm{\ge }\mathrm{-}\mathrm{2}$, $A\mathrm{:}\mathrm{U}$ and $B\mathrm{:}n\mathit{}\mathit{\text{-}}\mathit{}\mathrm{Type}$. The following map is anequivalence:

Proof.

Given that $B$ is $n$-truncated, any $f:A\to B$ can be extended to a map $\mathrm{𝖾𝗑𝗍}(f):\parallel A{\parallel }_n\to B$.The map $\mathrm{𝖾𝗑𝗍}(f)\circ {|\text{–}|}_n$ is equal to $f$, because for every $a:A$ we have $\mathrm{𝖾𝗑𝗍}(f)(|a{|}_n)=f(a)$ by definition.And the map $\mathrm{𝖾𝗑𝗍}(g\circ {|\text{–}|}_n)$ is equal to $g$, because they both send ${\left|a\right|}_n$ to $g(|a{|}_n)$.∎

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 $(\mathrm{\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\stackrel{𝑓}{\to }B\to \parallel B{\parallel }_n$ yields a map $\parallel f{\parallel }_n:\parallel A{\parallel }_n\to \parallel B{\parallel }_n$.By definition, we have a homotopy

$${\mathrm{𝗇𝖺𝗍}}_n^f:\prod _{a:A}\parallel f{\parallel }_n(|a{|}_n)=|f(a){|}_n,$$(7.3.4)

expressing naturality of the maps ${|\text{–}|}_n$.

Uniqueness implies functoriality laws such as $\parallel g\circ f{\parallel }_n=\parallel g{\parallel }_n\circ \parallel f{\parallel }_n$ and $\parallel {\mathrm{𝗂𝖽}}_A{\parallel }_n={\mathrm{𝗂𝖽}}_{\parallel A{\parallel }_n}$, with attendant coherence laws.We also have higher functoriality, for instance:

Lemma 7.3.5.

Given $f\mathrm{,}g\mathrm{:}A\mathrm{\to }B$ and a homotopy $h\mathrm{:}f\mathrm{\sim }g$, there is an induced homotopy $\mathrm{\parallel }h{\mathrm{\parallel }}_n\mathrm{:}\mathrm{\parallel }f{\mathrm{\parallel }}_n\mathrm{\sim }\mathrm{\parallel }g{\mathrm{\parallel }}_n$ such that the composite

$$HoT{T}_{f}i{g}_7\mathrm{.3.1}.png$$(7.3.5)

is equal to ${\mathrm{ap}}_{{\mathrm{|}\mathit{\text{–}}\mathrm{|}}_n}\mathit{}\mathrm{(}h\mathit{}\mathrm{(}a\mathrm{)}\mathrm{)}$.

Proof.

First, we indeed have a homotopy with components ${\mathrm{𝖺𝗉}}_{{|\text{–}|}_n}(h(a)):|f(a){|}_n=|g(a){|}_n$.Composing on either sides with the paths $|f(a){|}_n=\parallel f{\parallel }_n(|a{|}_n)$ and $|g(a){|}_n=\parallel g{\parallel }_n(|a{|}_n)$, which arise from the definitions of ${\parallel f\parallel }_n$ and ${\parallel g\parallel }_n$, we obtain a homotopy $(\parallel f{\parallel }_n\circ |\text{–}{|}_n)\sim (\parallel g{\parallel }_n\circ |\text{–}{|}_n)$, and hence an equality by function extensionality.But since $(\text{–}\circ {|\text{–}|}_n)$ is an equivalence, there must be a path $\parallel f{\parallel }_n=\parallel g{\parallel }_n$ 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 $\mathrm{|}\mathit{\text{–}}{\mathrm{|}}_n\mathrm{:}A\mathrm{\to }\mathrm{\parallel }A{\mathrm{\parallel }}_n$ 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 $\mathrm{𝖾𝗑𝗍}({\mathrm{𝗂𝖽}}_A):\parallel A{\parallel }_n\to A$.Then we have $\mathrm{𝖾𝗑𝗍}({\mathrm{𝗂𝖽}}_A)\circ {|\text{–}|}_n={\mathrm{𝗂𝖽}}_A:A\to A$ bydefinition. In order to prove that${|\text{–}|}_n\circ \mathrm{𝖾𝗑𝗍}({\mathrm{𝗂𝖽}}_A)={\mathrm{𝗂𝖽}}_{\parallel A{\parallel }_n}$, we only need to provethat ${|\text{–}|}_n\circ \mathrm{𝖾𝗑𝗍}({\mathrm{𝗂𝖽}}_A)\circ {|\text{–}|}_n={\mathrm{𝗂𝖽}}_{\parallel A{\parallel }_n}\circ {|\text{–}|}_n$.This is again true:

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 $\parallel -{\parallel }_n$ preserves finite products.

Theorem 7.3.8.

For any types $A$ and $B$, the induced map $\mathrm{\parallel }A\mathrm{\times }B{\mathrm{\parallel }}_n\mathrm{\to }\mathrm{\parallel }A{\mathrm{\parallel }}_n\mathrm{\times }\mathrm{\parallel }B{\mathrm{\parallel }}_n$ is an equivalence.

Proof.

It suffices to show that $\parallel A{\parallel }_n\times \parallel B{\parallel }_n$ has the same universal property as ${\parallel A\times B\parallel }_n$.Thus, let $C$ be an $n$-type; we have

$(\parallel A{\parallel }_n\times \parallel B{\parallel }_n\to C)$$=(\parallel A{\parallel }_n\to (\parallel B{\parallel }_n\to C))$

$=(\parallel A{\parallel }_n\to (B\to C))$

$=(A\to (B\to C))$

$=(A\times B\to C)$

using the universal properties of ${\parallel B\parallel }_n$ and ${\parallel A\parallel }_n$, 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 ${|\text{–}|}_n\times {|\text{–}|}_n$, as needed.∎

The following related fact about dependent sums is often useful.

Theorem 7.3.9.

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

$${\parallel \sum _{x:A}\parallel P(x){\parallel }_n\parallel }_n\simeq {\parallel \sum _{x:A}P(x)\parallel }_n.$$

Proof.

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

$\phi$$:{\parallel {\displaystyle \sum _{x:A}}\parallel P(x){\parallel }_n\parallel }_n\to {\parallel {\displaystyle \sum _{x:A}}P(x)\parallel }_n$

$\psi$$:{\parallel {\displaystyle \sum _{x:A}}P(x)\parallel }_n\to {\parallel {\displaystyle \sum _{x:A}}\parallel P(x){\parallel }_n\parallel }_n$

and homotopies $H:\phi \circ \psi \sim \mathrm{𝗂𝖽}$ and $K:\psi \circ \phi \sim \mathrm{𝗂𝖽}$ exhibiting them as quasi-inverses.We define $\phi$ by setting $\phi (|(x,|u{|}_n){|}_n):\equiv |(x,u){|}_n$.We define $\psi$ by setting $\psi (|(x,u){|}_n):\equiv |(x,|u{|}_n){|}_n$.Then we define $H(|(x,u){|}_n):\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{|(x,u){|}_n}$ and$K(|(x,|u{|}_n){|}_n):\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{|(x,|u{|}_n){|}_n}$.∎

Corollary 7.3.10.

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

$$\sum _{a:A}\parallel P(a){\parallel }_n\simeq {\parallel \sum _{a:A}P(a)\parallel }_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) forcoproducts 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:{\parallel x{=}_{A}y\parallel }_n\to \left(|x{|}_{n+1}{=}_{\parallel A{\parallel }_{n+1}}|y{|}_{n+1}\right)$$(7.3.11)

defined by

$$f(|p{|}_n):\equiv {\mathrm{𝖺𝗉}}_{{|\text{–}|}_{n+1}}(p).$$

This definition uses the recursion principle for ${\parallel \text{–}\parallel }_n$, which is correct because ${\parallel A\parallel }_{n+1}$ is $(n+1)$-truncated, so that thecodomain of $f$ is $n$-truncated.

Theorem 7.3.12.

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

$${\parallel x{=}_{A}y\parallel }_n\simeq \left(|x{|}_{n+1}{=}_{\parallel A{\parallel }_{n+1}}|y{|}_{n+1}\right).$$

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 anequality between ${\left|x\right|}_{n+1}$ and ${\left|y\right|}_{n+1}$.Thus, instead we generalize its type, in order to have general elements of the type ${\parallel A\parallel }_{n+1}$ instead of ${\left|x\right|}_{n+1}$ and ${\left|y\right|}_{n+1}$.Define $P:\parallel A{\parallel }_{n+1}\to \parallel A{\parallel }_{n+1}\to n\text{-}\mathrm{𝖳𝗒𝗉𝖾}$ by

$$P(|x{|}_{n+1},|y{|}_{n+1}):\equiv \parallel x{=}_{A}y{\parallel }_n$$

This definition is correct because $\parallel x{=}_{A}y{\parallel }_n$ is $n$-truncated, and $n\text{-}\mathrm{𝖳𝗒𝗉𝖾}$ is $(n+1)$-truncated byTheorem 7.1.11 (http://planetmath.org/71definitionofntypes#Thmprethm7).Now for every $u,v:\parallel A{\parallel }_{n+1}$, there is a map

$$\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}:P(u,v)\to \left(u{=}_{\parallel A{\parallel }_{n+1}}v\right)$$

defined for $u=|x{|}_{n+1}$ and $v=|y{|}_{n+1}$ and $p:x=y$ by

$$\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(|p{|}_n):\equiv {\mathrm{𝖺𝗉}}_{|\underset{¯}{}{|}_{n+1}}(p).$$

Since the codomain of $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$ is $n$-truncated, it suffices to define it only for $u$ and $v$ of this form, and then it’s just the samedefinition as before.We also define a function

$$r:\prod _{u:\parallel A{\parallel }_{n+1}}P(u,u)$$

by induction on $u$, where $r(|x{|}_{n+1}):\equiv |{\mathrm{𝗋𝖾𝖿𝗅}}_x{|}_n$.

Now we can define an inverse map

$$\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}:(u{=}_{\parallel A{\parallel }_{n+1}}v)\to P(u,v)$$

by

$$\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(p):\equiv {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{v\mapsto P(u,v)}(p,r(u)).$$

To show that the composite

$$(u{=}_{\parallel A{\parallel }_{n+1}}v)\stackrel{𝖽𝖾𝖼𝗈𝖽𝖾}{\to }P(u,v)\stackrel{𝖾𝗇𝖼𝗈𝖽𝖾}{\to }(u{=}_{\parallel A{\parallel }_{n+1}}v)$$

is the identity function, by path induction it suffices to check it for ${\mathrm{𝗋𝖾𝖿𝗅}}_u:u=u$, in which case what we need to know is that$\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(r(u))={\mathrm{𝗋𝖾𝖿𝗅}}_u$.But since this is an $n$-type, hence also an $(n+1)$-type, we may assume $u\equiv |x{|}_{n+1}$, in which case it follows by definitionof $r$ and $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}$.Finally, to show that

$$P(u,v)\stackrel{𝖾𝗇𝖼𝗈𝖽𝖾}{\to }(u{=}_{\parallel A{\parallel }_{n+1}}v)\stackrel{𝖽𝖾𝖼𝗈𝖽𝖾}{\to }P(u,v)$$

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

$\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(|p{|}_n))$$=\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}({\mathrm{𝖺𝗉}}_{|\underset{¯}{}{|}_{n+1}}(p))$

$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{v\mapsto P(|x{|}_{n+1},v)}({\mathrm{𝖺𝗉}}_{|\underset{¯}{}{|}_{n+1}}(p),|{\mathrm{𝗋𝖾𝖿𝗅}}_x{|}_n)$

$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{v\mapsto \parallel u=v{\parallel }_n}(p,|{\mathrm{𝗋𝖾𝖿𝗅}}_x{|}_n)$

$=|{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{v\mapsto (u=v)}(p,{\mathrm{𝗋𝖾𝖿𝗅}}_x){|}_n$

$=|p{|}_n.$

This completes the proof that $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$ and $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}$ are quasi-inverses.The stated result is then the special case where $u=|x{|}_{n+1}$ and $v=|y{|}_{n+1}$.∎

Corollary 7.3.13.

Let $n\mathrm{\ge }\mathrm{-}\mathrm{2}$ and $\mathrm{(}A\mathrm{,}a\mathrm{)}$ be a pointed type. Then

$${\parallel \mathrm{\Omega }(A,a)\parallel }_n=\mathrm{\Omega }\left(\parallel (A,a){\parallel }_{n+1}\right)$$

Proof.

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

Corollary 7.3.14.

Let $n\mathrm{\ge }\mathrm{-}\mathrm{2}$ and $k\mathrm{\ge }\mathrm{0}$ and $\mathrm{(}A\mathrm{,}a\mathrm{)}$ a pointed type. Then

$${\parallel {\mathrm{\Omega }}^k(A,a)\parallel }_n={\mathrm{\Omega }}^k\left(\parallel (A,a){\parallel }_{n+k}\right).$$

Proof.

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

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

Lemma 7.3.15.

Let $k\mathrm{,}n\mathrm{\ge }\mathrm{-}\mathrm{2}$ with $k\mathrm{\le }n$ and $A\mathrm{:}\mathrm{U}$. Then$\mathrm{\parallel }\mathrm{\parallel }A{\mathrm{\parallel }}_n{\mathrm{\parallel }}_k\mathrm{=}\mathrm{\parallel }A{\mathrm{\parallel }}_k$.

Proof.

We define two maps $f:\parallel \parallel A{\parallel }_n{\parallel }_k\to \parallel A{\parallel }_k$ and$g:\parallel A{\parallel }_k\to \parallel \parallel A{\parallel }_n{\parallel }_k$ by

$$f(||a{|}_n{|}_k):\equiv |a{|}_k\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}g(|a{|}_k):\equiv ||a{|}_n{|}_k.$$

The map $f$ is well-defined because ${\parallel A\parallel }_k$ is $k$-truncated and also$n$-truncated (because $k\le n$), and the map $g$ is well-defined because$\parallel \parallel A{\parallel }_n{\parallel }_k$ is $k$-truncated.

The composition $f\circ g:\parallel A{\parallel }_k\to \parallel A{\parallel }_k$ satisfies$(f\circ g)(|a{|}_k)=|a{|}_k$, hence $f\circ g={\mathrm{𝗂𝖽}}_{\parallel A{\parallel }_k}$.Similarly, we have $(g\circ f)(||a{|}_n{|}_k)=||a{|}_n{|}_k$ and hence $g\circ f={\mathrm{𝗂𝖽}}_{\parallel \parallel A{\parallel }_n{\parallel }_k}$.∎