Proposition 11.6.0.78 (0195)

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$