# Kerodon

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

Corollary 4.5.4.5. Suppose we are given a categorical pushout square of simplicial sets

$\xymatrix@R =50pt@C=50pt{ A \ar [r] \ar [d] & B \ar [d] \\ A' \ar [r] & B', }$

where the horizontal maps are monomorphisms. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category. For every diagram $A' \rightarrow \operatorname{\mathcal{C}}$, the restriction map $\operatorname{Fun}_{A'/}(B', \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}_{A/}(B,\operatorname{\mathcal{C}})$ is an equivalence of $\infty$-categories.

Proof. Proposition 4.5.4.4 guarantees that the diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(B', \operatorname{\mathcal{C}}) \ar [r] \ar [d] & \operatorname{Fun}(B, \operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Fun}(A', \operatorname{\mathcal{C}}) \ar [r] & \operatorname{Fun}( A, \operatorname{\mathcal{C}}) }$

is a categorical pullback square, and Corollary 4.4.5.3 guarantees that the vertical maps are isofibrations. The desired result now follows from Corollary 4.5.2.25. $\square$