"$X$ is $n$-truncated $\iff$ $\Omega X$ is $(n-1)$-truncated" for connected pointed $X$. (HTT, 7.2.2.11)

Question

In the proof of Lemma 7.2.2.11 of Higher Topos Theory, Lurie makes the following claim:

($\ast$) Let $n\geq1$ be an integer, let $\mathcal{X}$ be an $\infty$-topos, and let $1\to X$ be a pointed object of $\mathcal{X}$, where $X$ is connected. Then $X$ is $n$-truncated if and only if $\Omega X$ is $(n-1)$-truncated.

The "only if" part is clear from the definition of truncatedness (using the observation that, in the category of spaces, all components of loop spaces are homotopy equivalent to each other). However, I do not understand how one proves the "if" part. Lurie says that it suffices to show that $\pi_i(X)$ vanishes for $i>n$, but given that the relation between truncatedness and homotopy groups is somewhat subtle in $\infty$-topoi (as remarked in Remark 6.5.1.8 of HTT), I do not see why this is sufficient. Can anyone help me how to prove the "if" part of ($\ast$)? Thanks in advance.

Answer 1

We have that $X$ is $n$-truncated if and only if the diagonal $\delta_X : X \to X \times X$ is $(n-1)$-truncated (Lemma 5.5.6.15 of HTT). Because $X$ is connected, $1 \to X \times X$ is an effective epimorphism (e.g. by factorising it as $1 \to X \to X \times X$). By Proposition 6.2.3.17 of HTT, $\delta_X$ is $(n-1)$-truncated if and only if its pullback along $1 \to X \times X$ is. This is precisely the loop object $\Omega X \to 1$.

In the language of homotopy type theory one can formulate the above proof as follows. To show that $X$ is $n$-truncated one has to show that the identity type $x = x'$ is $(n-1)$-truncated for all $x,x' : X$. Say given $x, x' : X$. Because $X$ is connected, we merely have that $x$ and $x'$ are both the basepoint of $X$. Since being $(n-1)$-truncated is property (rather than structure), we can assume $x$ and $x'$ are both the basepoint of $X$. In this case $x = x'$ is the loop object $\Omega X$.