# Kerodon

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

Proposition 4.5.4.4. A commutative diagram of simplicial sets

4.30
$$\begin{gathered}\label{equation:categorical-pushout-to-categorical-pullback} \xymatrix@R =50pt@C=50pt{ A \ar [r] \ar [d] & A_0 \ar [d] \\ A_1 \ar [r] & A_{01} } \end{gathered}$$

is a categorical pushout square if and only if it satisfies the following condition:

$(\ast )$

For every $\infty$-category $\operatorname{\mathcal{C}}$, the diagram of $\infty$-categories

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

is a categorical pullback square.

Proof. Fix an $\infty$-category $\operatorname{\mathcal{C}}$. If the diagram of $\infty$-categories (4.31) is a categorical pullback square, then the diagram of cores

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(A,\operatorname{\mathcal{C}})^{\simeq } & \operatorname{Fun}( A_0, \operatorname{\mathcal{C}})^{\simeq } \ar [l] \\ \operatorname{Fun}(A_1, \operatorname{\mathcal{C}})^{\simeq } \ar [u] & \operatorname{Fun}( A_{01}, \operatorname{\mathcal{C}})^{\simeq } \ar [l] \ar [u] }$

is a homotopy pullback square (Proposition 4.5.2.12). Allowing $\operatorname{\mathcal{C}}$ to vary, we see that if $(\ast )$ is satisfied, then (4.30) is a categorical pushout square. For the converse, assume that (4.30) is a categorical pullback square. For every simplicial set $X$, the simplicial set $\operatorname{Fun}(X, \operatorname{\mathcal{C}})$ is an $\infty$-category (Theorem 1.4.3.7), so the diagram of Kan complexes

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

is a homotopy pullback square. Identifying (4.32) with the diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( X, \operatorname{Fun}(A, \operatorname{\mathcal{C}}))^{\simeq } & \operatorname{Fun}(X, \operatorname{Fun}(A_0, \operatorname{\mathcal{C}}) )^{\simeq } \ar [l] \\ \operatorname{Fun}(X,\operatorname{Fun}( A_1, \operatorname{\mathcal{C}}))^{\simeq } \ar [u] & \operatorname{Fun}(X, \operatorname{Fun}(A_{01}, \operatorname{\mathcal{C}}))^{\simeq } \ar [u] \ar [l] }$

and allowing $X$ to vary, we conclude that the diagram (4.31) is a categorical pullback square (Proposition 4.5.2.12). $\square$