# Kerodon

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

Corollary 4.5.4.6. Suppose we are given a pullback diagram of $\infty$-categories

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

where $q$ is an isofibration. If $F$ is an equivalence of $\infty$-categories, then $F'$ is also an equivalence of $\infty$-categories.

Proof. Let $X$ be an arbitrary simplicial set. Then we have a pullback diagram of $\infty$-categories

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}') \ar [d] \ar [r]^-{F'_{X}} & \operatorname{Fun}(X,\operatorname{\mathcal{C}}) \ar [d]^{q_ X} \\ \operatorname{Fun}(X,\operatorname{\mathcal{D}}') \ar [r]^-{F_ X} & \operatorname{Fun}(X,\operatorname{\mathcal{D}}), }$

where $q_{X}$ is also an isofibration (Corollary 4.4.5.6). Invoking Corollary 4.4.3.19, we conclude that the diagram of Kan complexes

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

is a homotopy pullback square. Since $F$ is an equivalence of $\infty$-categories, the morphism $F^{\simeq }_{X}$ is a homotopy equivalence of Kan complexes (Theorem 4.5.4.1). Applying Corollary 3.4.1.3, we conclude that $F'^{\simeq }_{X}$ is also a homotopy equivalence of Kan complexes. Allowing $X$ to vary, we conclude that $F'$ is an equivalence of $\infty$-categories. $\square$