Kerodon

Proof. We proceed by induction on $k$. If $k = 0$, the result is a reformulation of Example 3.5.9.4. Let us therefore assume that $k > 0$. Note that $\delta $ factors as a composition $X \hookrightarrow \operatorname{Fun}( \Delta ^ k, X ) \xrightarrow { R_ k } \operatorname{Fun}( \operatorname{\partial \Delta }^{k}, X)$, where the first map is a homotopy equivalence (see Example 3.2.4.2) and $R_{k}$ is a Kan fibration (Corollary 3.1.3.3). Consequently, $\delta $ is $(n-k)$-truncated if and only if the morphism $R_{k}$ is $(n-k)$-truncated. To carry out the inductive step, it will suffice to prove the following:

$(\ast )$

If $R_{k-1}: \operatorname{Fun}( \Delta ^{k-1}, X) \rightarrow \operatorname{Fun}( \operatorname{\partial \Delta }^{k-1}, X)$ is $m$-truncated, then $R_{k}: \operatorname{Fun}( \Delta ^{k}, X) \rightarrow \operatorname{Fun}( \operatorname{\partial \Delta }^{k}, X)$ is $(m-1)$-truncated. The converse holds for $m \geq -1$.

Assume first that $R_{k-1}$ is $m$-truncated. Note that we have a pullback diagram of restriction maps

Applying the criterion of Proposition 3.5.9.8, we conclude that $T$ is also $m$-truncated. Note that the composition $(T \circ R_{k} ): \operatorname{Fun}( \Delta ^{k}, X) \rightarrow \operatorname{Fun}( \Lambda ^{k}_{k}, X)$ is given by precomposition with the horn inclusion $\Lambda ^{k}_{k} \hookrightarrow \Delta ^{k}$, and is therefore a trivial Kan fibration (Corollary 3.1.3.6). In particular, $T \circ R_{k}$ is $(m-1)$-truncated, so Corollary 3.5.9.14 guarantees that $R_{k}$ is $(m-1)$-truncated by virtue of Corollary 3.5.9.14.

We now prove the converse. Assume that $R_{k}$ is $(m-1)$-truncated and that $m \geq -1$; we wish to show that $R_{k-1}$ is $m$-truncated. Let $\operatorname{Fun}'( \operatorname{\partial \Delta }^{k}, X )$ denote the summand of $\operatorname{Fun}( \operatorname{\partial \Delta }^{k}, X)$ whose vertices are nullhomotopic maps $\operatorname{\partial \Delta }^{k} \rightarrow X$, and let $T': \operatorname{Fun}'( \operatorname{\partial \Delta }^{k}, X) \rightarrow \operatorname{Fun}( \Lambda ^{k}_{k}, X)$ be the restriction map. As above, the composition $T' \circ R_{k}$ is a trivial Kan fibration, and therefore $m$-truncated Applying Corollary 3.5.9.14, we conclude that $T'$ is $m$-truncated.

Fix a morphism $\sigma _0: \operatorname{\partial \Delta }^{k-1} \rightarrow X$, and set $Y = \{ \sigma _0 \} \times _{ \operatorname{Fun}( \operatorname{\partial \Delta }^{k-1}, X) } \operatorname{Fun}( \Delta ^{k-1}, X)$; by virtue of Proposition 3.5.9.8, it will suffice to show that $Y$ is $m$-truncated. We first consider the case $m \geq 0$. By virtue of Remark 3.5.7.11, it will suffice to show that every connected component $Z \subseteq Y$ is $m$-truncated. Fix a vertex of $Z$, corresponding to a map $\sigma : \Delta ^{k-1} \rightarrow X$ extending $\sigma _0$. Choose an extension of $\sigma $ to a $k$-simplex $\tau : \Delta ^{k} \rightarrow X$ (for example, we can take $\tau $ to be the degenerate $k$-simplex $s^{k-1}_{k-1}(\sigma )$), and set $\tau _0 = \tau |_{ \Lambda ^{k}_{k} }$. Since (3.80) is a pullback square, it induces an isomorphism from $Y$ to the fiber $T^{-1} \{ \tau _0 \} = \{ \tau _0 \} \times _{ \operatorname{Fun}( \Lambda ^{k}_{k}, X) } \operatorname{Fun}( \operatorname{\partial \Delta }^{k}, X)$. By construction, this isomorphism identifies $Z$ to a connected component of the fiber $T'^{-1} \{ \tau _0 \} = \times _{ \operatorname{Fun}( \Lambda ^{k}_{k}, X) } \operatorname{Fun}( \operatorname{\partial \Delta }^{k}, X)$. Our assumption that $T'$ is $m$-truncated guarantees that this fiber $T'^{-1} \{ \tau _0 \} $ is $m$-truncated (Proposition 3.5.9.8), so that $Z$ is also $m$-truncated (Remark 3.5.7.11).

We now treat the case $m = -1$: in this case, we wish to show that $Y$ is either empty or contractible. Let us assume that $Y$ is nonempty: that is, $\sigma _0$ can be extended to a $(k-1)$-simplex $\sigma : \Delta ^{k-1} \rightarrow X$. Define $\tau $ and $\tau _0$ as above, so that we can identify $Y$ with the fiber $T^{-1} \{ \tau _0 \} $. We will complete the proof by showing that $T$ is a trivial Kan fibration. Since $T$ is a Kan fibration, it will suffice to show that it is a homotopy equivalence (Proposition 3.2.7.2). Since $T \circ R_{k}$ is a homotopy equivalence, we are reduced to showing that $R_{k}$ is a homotopy equivalence. This is a reformulation of our hypothesis that $R_{k}$ is $(m-1)$-truncated (see Example 3.5.9.2). $\square$