# Kerodon

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

Corollary 4.5.4.7. Suppose we are given a commutative diagram of $\infty$-categories

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}' \ar [d]^-{q'} \ar [r]^-{F'} & \operatorname{\mathcal{C}}\ar [d]^{q} \\ \operatorname{\mathcal{D}}' \ar [r]^-{F} & \operatorname{\mathcal{D}}, }$

where $q'$ and $q$ are isofibrations and the functors $F$ and $F'$ are equivalences of $\infty$-categories. Then, for every object $D' \in \operatorname{\mathcal{D}}'$ having image $D = F(D') \in \operatorname{\mathcal{D}}$, the induced functor

$\operatorname{\mathcal{C}}'_{D'} = \{ D'\} \times _{\operatorname{\mathcal{D}}'} \operatorname{\mathcal{C}}' \rightarrow \{ D\} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}= \operatorname{\mathcal{C}}_{D}$

is an equivalence of $\infty$-categories.

Proof. For every simplicial set $X$, we have a commutative diagram of Kan complexes

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}')^{\simeq } \ar [r] \ar [d] & \operatorname{Fun}(X,\operatorname{\mathcal{C}})^{\simeq } \ar [d] \\ \operatorname{Fun}(X,\operatorname{\mathcal{D}}')^{\simeq } \ar [r] & \operatorname{Fun}(X,\operatorname{\mathcal{D}})^{\simeq }. }$

Our assumption that $F$ and $F'$ are equivalences of $\infty$-categories guarantee that the horizontal maps are homotopy equivalences (Theorem 4.5.4.1), and our assumption that $q$ and $q'$ are isofibrations guarantee that the vertical maps are Kan fibrations (Proposition 4.4.3.7). Let $\underline{D} \in \operatorname{Fun}(X,\operatorname{\mathcal{D}})$ and $\underline{D}' \in \operatorname{Fun}(X, \operatorname{\mathcal{D}}')$ be the constant diagrams taking the values $D$ and $D'$, respectively, so that the induced map of fibers

$\theta : \{ \underline{D}' \} \times _{ \operatorname{Fun}(X,\operatorname{\mathcal{D}}')^{\simeq } } \operatorname{Fun}(X, \operatorname{\mathcal{C}}')^{\simeq } \rightarrow \{ \underline{D} \} \times _{ \operatorname{Fun}(X,\operatorname{\mathcal{D}})^{\simeq } } \operatorname{Fun}(X, \operatorname{\mathcal{C}})^{\simeq }$

is also a homotopy equivalence (Proposition 3.2.8.1). Using Corollary 4.4.3.20 (and Corollary 4.4.5.6), we can identify $\theta$ with the natural map $\operatorname{Fun}(X, \operatorname{\mathcal{C}}'_{D'})^{\simeq } \rightarrow \operatorname{Fun}(X, \operatorname{\mathcal{C}}_{D})^{\simeq }$. Allowing $X$ to vary and applying Theorem 4.5.4.1, we conclude that the functor $\operatorname{\mathcal{C}}'_{D'} \rightarrow \operatorname{\mathcal{C}}_{D}$ is an equivalence of $\infty$-categories. $\square$