# Kerodon

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

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

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

where $f$ is a categorical equivalence. Then (4.20) is a categorical pushout diagram 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.21
\begin{equation} \label{diagram:categorical-pushout-lemma} \begin{gathered} \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(A,\operatorname{\mathcal{C}})^{\simeq } & \operatorname{Fun}(B,\operatorname{\mathcal{C}})^{\simeq } \ar [l]_{u} \\ \operatorname{Fun}(C,\operatorname{\mathcal{C}})^{\simeq } \ar [u] & \operatorname{Fun}(D,\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.2.8). Applying Corollary 3.4.1.3, we conclude that (4.21) is a homotopy pullback square if and only if $u'$ is a homotopy equivalence of Kan complexes. Consequently, (4.20) 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}(D, \operatorname{\mathcal{C}})^{\simeq } \rightarrow \operatorname{Fun}(C, \operatorname{\mathcal{C}})^{\simeq }$. By virtue of Proposition 4.5.2.8, this is equivalent to the requirement that $f'$ is a weak homotopy equivalence. $\square$