# Kerodon

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

Proposition 4.5.2.17 (Homotopy Invariance). Suppose we are given a commutative diagram of $\infty$-categories

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{01} \ar [dr]^{ F_{01} } \ar [rr] \ar [dd] & & \operatorname{\mathcal{C}}_{0} \ar [dd] \ar [dr]^{F_1} & \\ & \operatorname{\mathcal{D}}_{01} \ar [rr] \ar [dd] & & \operatorname{\mathcal{D}}_{0} \ar [dd] \\ \operatorname{\mathcal{C}}_{1} \ar [rr] \ar [dr]^{ F_1 } & & \operatorname{\mathcal{C}}\ar [dr]^{F} & \\ & \operatorname{\mathcal{D}}_{1} \ar [rr] & & \operatorname{\mathcal{D}}, }$

where $F_0$, $F_1$, and $F$ are equivalences of $\infty$-categories. Then any two of the following conditions imply the third:

$(1)$

The back face

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{01} \ar [r] \ar [d] & \operatorname{\mathcal{C}}_0 \ar [d] \\ \operatorname{\mathcal{C}}_1 \ar [r] & \operatorname{\mathcal{C}}}$

is a categorical pullback square.

$(2)$

The front face

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{D}}_{01} \ar [r] \ar [d] & \operatorname{\mathcal{D}}_0 \ar [d] \\ \operatorname{\mathcal{D}}_1 \ar [r] & \operatorname{\mathcal{D}}}$

is a categorical pullback square.

$(3)$

The functor $F_{01}$ is an equivalence of $\infty$-categories.

Proof. Using Proposition 4.5.1.22, we see that $(3)$ is equivalent to the following:

$(3')$

For every simplicial set $X$, the functor $F_{01}$ induces a homotopy equivalence of Kan complexes $\operatorname{Fun}(X, \operatorname{\mathcal{C}}_{01} )^{\simeq } \rightarrow \operatorname{Fun}(X, \operatorname{\mathcal{D}}_{01})^{\simeq }$.

The equivalences $(1) \Leftrightarrow (2) \Leftrightarrow (3')$ now follow by combining Proposition 4.5.2.12 with Corollary 3.4.1.12. $\square$