# Kerodon

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

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

4.22
$$\label{diagram:categorical-pushout-square1} \begin{gathered} \xymatrix@R =50pt@C=50pt{ A \ar [r]^-{f} \ar [d] & B \ar [d] \\ C \ar [r] & D, } \end{gathered}$$

where $f$ is a monomorphism. Then (4.22) is a categorical pushout square if and only if the induced map $\rho : C \coprod _{A} B \rightarrow D$ is a categorical equivalence of simplicial sets.

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

4.23
$$\label{diagram:categorical-pushout-lemma2} \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] \ar [u] } \end{gathered}$$

where $u$ is a Kan fibration (Corollary 4.4.5.4). It follows that the diagram (4.23) is a homotopy pullback square if and only if the induced map

$\theta : \operatorname{Fun}(D, \operatorname{\mathcal{C}})^{\simeq } \rightarrow \operatorname{Fun}(C,\operatorname{\mathcal{C}})^{\simeq } \times _{ \operatorname{Fun}(A,\operatorname{\mathcal{C}})^{\simeq }} \operatorname{Fun}(B,\operatorname{\mathcal{C}})^{\simeq }$

is a weak homotopy equivalence (Example 3.4.1.5). By virtue of Corollary 4.4.4.6, we can identify $\theta$ with the map $\operatorname{Fun}(D, \operatorname{\mathcal{C}})^{\simeq } \rightarrow \operatorname{Fun}( B \coprod _{A} C, \operatorname{\mathcal{C}})^{\simeq }$ given by precomposition with $\rho$. It follows that the diagram (4.22) is a categorical pushout square if and only if, for every $\infty$-category $\operatorname{\mathcal{C}}$, the induced map $\operatorname{Fun}(D, \operatorname{\mathcal{C}})^{\simeq } \rightarrow \operatorname{Fun}( C \coprod _{A} B, \operatorname{\mathcal{C}})^{\simeq }$ is a homotopy equivalence of Kan complexes. By virtue of Proposition 4.5.2.8, this is equivalent to the requirement that $\rho$ is a categorical equivalence. $\square$