Proposition 11.9.5.6. Suppose we are given a commutative diagram of Kan complexes
\[ \xymatrix@R =50pt@C=50pt{ \cdots \ar [r]^-{ p_3} & X(3) \ar [d]^{ f_3} \ar [r]^-{ p_2} & X(2) \ar [r]^-{p_1} \ar [d]^{f_2} & X(1) \ar [r]^-{ p_0} \ar [d]^{f_1} & X(0) \ar [d]^{f_0} \\ \cdots \ar [r]^-{ q_3 } & Y(3) \ar [r]^-{ q_2} & Y(2) \ar [r]^-{q_1} & Y(1) \ar [r]^-{ q_0 } & Y(0). } \]
Assume that for each $n \geq 0$, the morphisms $p_ n$ and $q_ n$ are Kan fibrations, and the morphism $f_ n$ is a homotopy equivalence. Then the induced map $f: \varprojlim \{ X(n) \} _{n \geq 0} \rightarrow \varprojlim \{ Y(n) \} _{n \geq 0}$ is a homotopy equivalence of Kan complexes.
Proof.
Set $X = \varprojlim \{ X(n) \} _{n \geq 0}$ and $Y = \varprojlim \{ Y(n) \} _{n \geq 0}$, so that $X$ and $Y$ are Kan complexes (Corollary 11.9.5.2). By virtue of Remark 3.4.0.6, it will suffice to show that for each vertex $y \in Y$, the homotopy fiber $F = X \times ^{\mathrm{h}}_{Y} \{ y\} $ is a contractible Kan complex. For each $n \geq 0$, set $F(n) = X(n) \times ^{\mathrm{h}}_{Y(n)} \{ y\} $, so that $F$ can be identified with the limit $\varprojlim \{ F(n) \} _{n \geq 0}$. Since $f_{n}$ is a homotopy equivalence, $F(n)$ is a contractible Kan complex (Remark 3.4.0.6). By virtue of Corollary None, it will suffice to show that each of the transition maps $\theta _{n}: F(n+1) \rightarrow F(n)$ is a Kan fibration. Unwinding the definitions, we see that $\theta _{n}$ factors as a composition
\[ X(n+1) \times _{Y(n+1)}^{\mathrm{h}} \{ y\} \xrightarrow {\theta '} X(n+1) \times _{Y(n)}^{\mathrm{h}} \{ y\} \xrightarrow {\theta ''} X(n) \times _{ Y(n) }^{\mathrm{h}} \{ y\} . \]
Here $\theta '$ is a pullback of the map $p_{n}$ (and therefore a Kan fibration by assumption), while $\theta ''$ is a pullback of the map
\[ \operatorname{Fun}( \Delta ^1, Y(n+1) ) \rightarrow \operatorname{Fun}( \operatorname{\partial \Delta }^1, Y(n+1) ) \times _{ \operatorname{Fun}( \operatorname{\partial \Delta }^1, Y(n) ) } \operatorname{Fun}( \Delta ^1, Y(n) ), \]
and is therefore a Kan fibration by virtue of Theorem 3.1.3.1.
$\square$