Corollary 3.5.2.7. Let $n$ be an integer, and suppose we are given a homotopy pushout square of simplicial sets
If $f$ is $n$-connective, then $f'$ is also $n$-connective.
Corollary 3.5.2.7. Let $n$ be an integer, and suppose we are given a homotopy pushout square of simplicial sets
If $f$ is $n$-connective, then $f'$ is also $n$-connective.
Proof. Using Proposition 3.1.7.1, we can factor $f$ as a composition $X \xrightarrow {i} \overline{X} \xrightarrow {\overline{f}} Y$, where $i$ is anodyne and $\overline{f}$ is a Kan fibration. Replacing $X$ by $\overline{X}$ and $X'$ by the pushout $X' \coprod _{X} \overline{X}$, we are reduced to proving Corollary 3.5.2.7 in the special case where $f$ is a Kan fibration. In this case, we can use Corollary 3.5.2.4 to factor $f$ as a composition $X \xrightarrow { \widetilde{f} } \widetilde{Y} \xrightarrow {q} Y$, where $q$ is a trivial Kan fibration and $\widetilde{f}$ is a monomorphism which is bijective on $k$-simplices for $k \leq n$. In this case, our assumption that (3.70) is a homotopy pushout square guarantees that the induced map $X' \coprod _{X} \widetilde{Y} \rightarrow Y'$ is a weak homotopy equivalence (Proposition 3.4.2.11). Consequently, to show that $f'$ is $n$-connective, it will suffice to show that the inclusion map $j: X' \hookrightarrow X' \coprod _{X} \widetilde{Y}$ is $n$-connective (Corollary 3.5.1.28). This is a special case of Corollary 3.5.2.2, since $j$ is bijective on $k$-simplices for $k \leq n$. $\square$