# Kerodon

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

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

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

where $f$ is a monomorphism. Then (4.35) is a categorical pushout square if and only if the induced map $\rho : A_0 \coprod _{A} A_1 \rightarrow A_{01}$ is a categorical equivalence of simplicial sets.

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

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

where $u$ is an isofibration (Corollary 4.4.5.3). It follows that the diagram (4.36) is a categorical pullback square if and only if the induced map

$\theta _{\operatorname{\mathcal{C}}}: \operatorname{Fun}(A_{01}, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(A_0,\operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A,\operatorname{\mathcal{C}})} \operatorname{Fun}(A_1,\operatorname{\mathcal{C}}) \simeq \operatorname{Fun}( A_0 \coprod _{A} A_1, \operatorname{\mathcal{C}})$

is an equivalence of $\infty$-categories (Proposition 4.5.2.20). Using Proposition 4.5.4.4, we see that this condition is satisfied for every $\infty$-category $\operatorname{\mathcal{C}}$ if and only if (4.35) is a categorical pushout square. The desired result now follows from Proposition 4.5.3.8. $\square$