Kerodon

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

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.31. $\square$