Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Corollary 3.5.9.11. Let $n$ be an integer and suppose we are given a homotopy pullback diagram of Kan complexes

3.79
\begin{equation} \begin{gathered}\label{equation:homotopy-pullback-square-truncatedness} \xymatrix@R =50pt@C=50pt{ X \ar [r] \ar [d]^{f} & X' \ar [d]^{f'} \\ Y \ar [r]^-{g} & Y'. } \end{gathered} \end{equation}

If $f'$ is $n$-truncated, then $f$ is also $n$-truncated. The converse holds if $\pi _0(g)$ is surjective.

Proof. Using Proposition 3.1.7.1, we can reduce to the case where $f$ and $f'$ are Kan fibrations. In this case, our assumption that (3.79) is a homotopy pullback square guarantees that for each vertex $y \in Y$, the induced map of fibers $X_{y} \rightarrow X'_{g(y)}$ is a homotopy equivalence (Example 3.4.1.4) In particular, $X_{y}$ is $n$-truncated if and only if $X'_{g(y)}$ is $n$-truncated (Corollary 3.5.7.12). The desired result now follows from the criterion of Proposition 3.5.9.8 (together with Remark 3.5.9.9). $\square$