Kerodon

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

Proposition 4.8.9.7. Suppose we are given a categorical pushout square of simplicial sets

4.89
\begin{equation} \begin{gathered}\label{equation:pushout-of-categorically-connective} \xymatrix@C =50pt@R=50pt{ A \ar [d]^{f} \ar [r] & A' \ar [d]^{f'} \\ B \ar [r] & B', } \end{gathered} \end{equation}

where $f$ is categorically $n$-connective. Then $f'$ is also categorically $n$-connective.

Proof. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an essentialy $(n-1)$-categorical functor of $\infty $-categories, and consider the cubical diagram

\[ \xymatrix@C =50pt@R=50pt{ \operatorname{Fun}(B', \operatorname{\mathcal{C}}) \ar [dr] \ar [rr] \ar [dd] & & \operatorname{Fun}(B, \operatorname{\mathcal{C}}) \ar [dr] \ar [dd] & \\ & \operatorname{Fun}(B', \operatorname{\mathcal{D}}) \ar [rr] \ar [dd] & & \operatorname{Fun}(B, \operatorname{\mathcal{D}}) \ar [dd] \\ \operatorname{Fun}(A', \operatorname{\mathcal{C}}) \ar [rr] \ar [dr] & & \operatorname{Fun}(A, \operatorname{\mathcal{C}}) \ar [dr] & \\ & \operatorname{Fun}(A', \operatorname{\mathcal{D}}) \ar [rr] & & \operatorname{Fun}(A, \operatorname{\mathcal{D}}). } \]

Our assumption that $f$ is categorically $n$-connective guarantees that the right face is a categorical pullback square, and our assumption on (4.89) guarantees that the front and back faces are categorical pullback squares. Applying Proposition 4.5.2.18, we conclude that the left face is also a categorical pullback square. $\square$