Proposition 4.5.4.10 (01FC)

Proposition 4.5.4.10. Suppose we are given a commutative diagram of simplicial sets

4.34

\begin{equation} \label{diagram:categorical-pushout-square0} \begin{gathered} \xymatrix@R =50pt@C=50pt{ A \ar [r]^-{f} \ar [d] & A_0 \ar [d] \\ A_1 \ar [r]^-{f'} & A_{01} } \end{gathered} \end{equation}

where $f$ is a categorical equivalence. Then (4.34) is a categorical pushout square if and only if $f'$ is a categorical equivalence.

Proof. For every $\infty $-category $\operatorname{\mathcal{C}}$, we obtain a commutative diagram of simplicial sets

4.35

\begin{equation} \label{diagram:categorical-pushout-lemma} \begin{gathered} \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(A,\operatorname{\mathcal{C}})^{\simeq } & \operatorname{Fun}(A_0,\operatorname{\mathcal{C}})^{\simeq } \ar [l]_{u} \\ \operatorname{Fun}(A_1,\operatorname{\mathcal{C}})^{\simeq } \ar [u] & \operatorname{Fun}(A_{01},\operatorname{\mathcal{C}})^{\simeq }, \ar [l]_{u'} \ar [u] } \end{gathered} \end{equation}

where $u$ is a homotopy equivalence of Kan complexes (Proposition 4.5.3.8). Applying Corollary 3.4.1.5, we conclude that (4.35) is a homotopy pullback square if and only if $u'$ is a homotopy equivalence of Kan complexes. Consequently, (4.34) is a categorical pushout square if and only if, for every $\infty $-category $\operatorname{\mathcal{C}}$, the composition with $f'$ induces a homotopy equivalence $\operatorname{Fun}(A_{01}, \operatorname{\mathcal{C}})^{\simeq } \rightarrow \operatorname{Fun}(A_1, \operatorname{\mathcal{C}})^{\simeq }$. By virtue of Proposition 4.5.3.8, this is equivalent to the requirement that $f'$ is a categorical equivalence. $\square$