Kerodon

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

Lemma 5.6.9.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \Delta ^1$ be a cocartesian fibration having fibers $\operatorname{\mathcal{E}}_{0} = \{ 0\} \times _{\Delta ^1} \operatorname{\mathcal{E}}$ and $\operatorname{\mathcal{E}}_{1} = \{ 1\} \times _{\Delta ^1} \operatorname{\mathcal{E}}$. Then the restriction map

\[ \theta : \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^1 ) \rightarrow \operatorname{TW}( \operatorname{\mathcal{E}}_0 \amalg \operatorname{\mathcal{E}}_{1} / \operatorname{\partial \Delta }^{1} ) \]

is a trivial Kan fibration of simplicial sets.

Proof. It follows from Lemma 5.6.8.10 that $\theta $ is a Kan fibration; we wish to show that it is a trivial Kan fibration. Fix a pair of small $\infty $-categories $\operatorname{\mathcal{D}}_0$ and $\operatorname{\mathcal{D}}_1$. Set $\operatorname{\mathcal{E}}'_0 = \{ \operatorname{\mathcal{D}}_0 \} \times _{\operatorname{\mathcal{QC}}} \operatorname{\mathcal{QC}}_{\operatorname{Obj}}$ and $\operatorname{\mathcal{E}}'_1 = \{ \operatorname{\mathcal{D}}_1 \} \times _{ \operatorname{\mathcal{QC}}} \operatorname{\mathcal{QC}}_{\operatorname{Obj}}$, and let $\operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_0 )$ and $\operatorname{Equiv}( \operatorname{\mathcal{E}}_1, \operatorname{\mathcal{E}}'_1 )$ be the Kan complexes introduced in Example 5.6.8.2, so that the fiber

\[ \{ (\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \} \times _{ \operatorname{Fun}( \operatorname{\partial \Delta }^1, \operatorname{\mathcal{QC}}) } \operatorname{TW}( \operatorname{\mathcal{E}}_0 \amalg \operatorname{\mathcal{E}}_1 / \operatorname{\partial \Delta }^1 ) \]

can be identified with the product $\operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_0) \times \operatorname{Equiv}( \operatorname{\mathcal{E}}_{1}, \operatorname{\mathcal{E}}'_1 )$. Let $\operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^{1})_{\operatorname{\mathcal{D}}_0,\operatorname{\mathcal{D}}_1}$ denote the fiber product $\{ (\operatorname{\mathcal{D}}_0,\operatorname{\mathcal{D}}_1) \} \times _{ \operatorname{Fun}( \operatorname{\partial \Delta }^1, \operatorname{\mathcal{QC}}) } \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^1)$, so that $\theta $ restricts to a Kan fibration

\[ \theta _{\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1}: \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^{1})_{\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1} \rightarrow \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_0 ) \times \operatorname{Equiv}( \operatorname{\mathcal{E}}_1, \operatorname{\mathcal{E}}'_1 ). \]

Note that every fiber of $\theta $ can also be viewed as a fiber of $\theta _{\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1}$ for suitably chosen $\infty $-categories $\operatorname{\mathcal{D}}_0$ and $\operatorname{\mathcal{D}}_1$. Consequently, to show that $\theta $ is a trivial Kan fibration, it will suffice to show that each of the morphisms $\theta _{\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1}$ is a trivial Kan fibration (Proposition 3.2.6.15), or equivalently that it is a homotopy equivalence (Corollary 3.2.7.4).

For the remainder of the proof, we will regard the $\infty $-categories $\operatorname{\mathcal{D}}_0$ and $\operatorname{\mathcal{D}}_1$ as fixed. Let $\operatorname{\mathcal{B}}^{+}$ denote the fiber product

\[ \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0 , \operatorname{\mathcal{D}}_1) \times _{ \operatorname{Fun}( \Delta ^1 \times \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{QC}})^{\simeq } } \operatorname{Fun}( \Delta ^1 \times \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )^{\simeq }. \]

Let $\pi ^{+}: \operatorname{\mathcal{B}}^{+} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1)$ be given by projection onto the first factor, and let

\[ r_{0}^{+}: \operatorname{\mathcal{B}}^{+} \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_0)^{\simeq } \quad \quad r^{+}_1: \operatorname{\mathcal{B}}^{+} \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_1)^{\simeq } \]

be given by restriction to the simplicial subsets $\{ 0\} \times \operatorname{\mathcal{E}}_{0}$ and $\{ 1\} \times \operatorname{\mathcal{E}}_{0}$, respectively. Combining Propositions 4.4.5.1 and 4.4.3.7, we deduce that the map

\[ (r^{+}_0, r^{+}_1, \pi ^{+}): \operatorname{\mathcal{B}}^{+} \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0})^{\simeq } \times \operatorname{Fun}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{E}}'_{1})^{\simeq } \times \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \]

is a Kan fibration. In particular, the simplicial set $\operatorname{\mathcal{B}}^{+}$ is a Kan complex.

Let $\operatorname{\mathcal{B}}$ denote the summand $\operatorname{\mathcal{B}}^{+}$ spanned by those pairs $(e, \widetilde{e})$, where $e: \operatorname{\mathcal{D}}_0 \rightarrow \operatorname{\mathcal{D}}_1$ is a functor and $\widetilde{e}: \Delta ^1 \times \operatorname{\mathcal{E}}_{0} \rightarrow \operatorname{\mathcal{QC}}_{\operatorname{Obj}}$ is a morphism fitting into a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \Delta ^1 \times \operatorname{\mathcal{E}}_{0} \ar [r]^-{ \widetilde{e} } \ar [d] & \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \ar [d]^{V} \\ \Delta ^1 \ar [r]^-{e} & \operatorname{\mathcal{QC}}} \]

which satisfies the following pair of conditions:

  • The restriction $\widetilde{e}|_{ \{ 0\} \times \operatorname{\mathcal{E}}_0 }: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}'_{0}$ is an equivalence of $\infty $-categories.

  • For each object $Z \in \operatorname{\mathcal{E}}_{0}$, the composite map

    \[ \Delta ^1 \times \{ Z\} \hookrightarrow \Delta ^1 \times \operatorname{\mathcal{E}}_0 \xrightarrow { \widetilde{e} } \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \]

    is a $V$-cocartesian morphism of $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$.

Condition $(i)$ ensures that $r_{0}^{+}$ restricts to a morphism of Kan complexes $r_0: \operatorname{\mathcal{B}}\rightarrow \operatorname{Equiv}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{E}}'_{0} )$. Moreover, $\pi ^{+}$ and $r_{1}^{+}$ restrict to morphisms $\pi : \operatorname{\mathcal{B}}\rightarrow \operatorname{Hom}_{\operatorname{\mathcal{QC}}}(\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1)$ and $r_{1}: \operatorname{\mathcal{B}}\rightarrow \operatorname{Fun}(\operatorname{\mathcal{E}}_{0},\operatorname{\mathcal{E}}'_1)^{\simeq }$, respectively. Since $\operatorname{\mathcal{B}}$ is a summand of $\operatorname{\mathcal{B}}^{+}$, the map

\[ (r_0, r_1,\pi ): \operatorname{\mathcal{B}}\rightarrow \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_0) \times \operatorname{Fun}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{E}}'_1)^{\simeq } \times \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \]

is also a Kan fibration.

It follows from Theorem 5.2.1.1 that composition with $V$ induces a cocartesian fibration $V': \operatorname{Fun}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}})$. Moreover, a morphism of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )$ is $V'$-cocartesian if and only if it corresponds to a morphism of simplicial sets $\widetilde{e}: \Delta ^1 \times \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{QC}}_{\operatorname{Obj}}$ satisfying condition $(ii)$. Let $\operatorname{Fun}'( \Delta ^1 \times \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}})$ denote the full subcategory of $\operatorname{Fun}( \Delta ^1 \times \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )$ spanned by morphisms which satisfy this condition. Unwinding the definitions, we have a pullback square

\[ \xymatrix@R =50pt@C=-70pt{ & \operatorname{\mathcal{B}}\ar [dl]_{ (r_0, \pi ) } \ar [dr] & \\ \operatorname{Equiv}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \ar [dr] & & \operatorname{Fun}'( \Delta ^1 \times \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}}) \ar [dl] \\ & \operatorname{Fun}( \{ 0\} \times \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \times _{ \operatorname{Fun}( \{ 0\} \times \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}) } \operatorname{Fun}( \Delta ^1 \times \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}), & } \]

where the bottom right map is a trivial Kan fibration (Proposition 5.2.1.3). It follows that the map $(r_0, \pi ): \operatorname{\mathcal{B}}\rightarrow \operatorname{Equiv}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1)$ is a trivial Kan fibration of simplicial sets.

Let $s: \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1 ) \rightarrow \operatorname{\mathcal{B}}$ be a section of the trivial Kan fibration $(r_0, \pi )$, and let $T$ denote the composite map

\[ \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \xrightarrow {s} \operatorname{\mathcal{B}}\xrightarrow { (r_0, r_1) } \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{1} )^{\simeq }. \]

For every equivalence of $\infty $-categories $F: \operatorname{\mathcal{E}}_{0} \rightarrow \operatorname{\mathcal{E}}'_{0}$, we can regard $T|_{ \{ F\} \times \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) }$ as a morphism of Kan complexes $T_{F}: \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{E}}'_{1} )^{\simeq }$. Unwinding the definitions, we can identify $T_{F}$ with the composition

\[ \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \xrightarrow {T'} \operatorname{Fun}( \operatorname{\mathcal{E}}'_{0}, \operatorname{\mathcal{E}}'_{1} )^{\simeq } \xrightarrow { \circ F } \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{1} )^{\simeq }, \]

where $T'$ is given by parametrized covariant transport for the cocartesian fibration $V: \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \rightarrow \operatorname{\mathcal{QC}}$ (Definition 5.2.8.1). It follows from Proposition 5.5.6.14 that $T'$ is a homotopy equivalence. Our assumption that $F$ is an equivalence of $\infty $-categories then guarantees that $T_{F}$ is also a homotopy equivalence. Allowing $F \in \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0} )$ to vary and applying Proposition 3.2.8.1, we conclude that $T$ is a homotopy equivalence. Since $s$ is homotopy inverse to the trivial Kan fibration $(r_0, \pi )$, it is also a homotopy equivalence. Applying the two-out-of-three property (Remark 3.1.6.7), we conclude that the map

\[ (r_0, r_1): \operatorname{\mathcal{B}}\rightarrow \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0}) \times \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{1} )^{\simeq } \]

is also a homotopy equivalence. Since $(r_0, r_1)$ is also a Kan fibration, it is a trivial Kan fibration (Proposition 3.3.7.4).

Using Proposition 5.2.2.8, we can choose a functor $\lambda : \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}_{1}$ and a natural transformation $h: \Delta ^1 \times \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}$ which witnesses $\lambda $ as given by covariant transport along the nondegenerate edge of $\Delta ^1$ (in the sense of Definition 5.2.2.4). Form a pullback diagram

5.61
\begin{equation} \begin{gathered}\label{equation:universality-formulation-0} \xymatrix@R =50pt@C=50pt{ \widetilde{\operatorname{\mathcal{B}}} \ar [r] \ar [d]^{ ( \widetilde{r}_0, \widetilde{r}_1)} & \operatorname{\mathcal{B}}\ar [d]^{ (r_0, r_1) } \\ \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Equiv}( \operatorname{\mathcal{E}}_{1}, \operatorname{\mathcal{E}}'_{1}) \ar [r]^-{\circ \lambda } & \operatorname{Equiv}( \operatorname{\mathcal{E}}_{0}, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Fun}(\operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{1} )^{\simeq }. } \end{gathered} \end{equation}

Let $\operatorname{\mathcal{M}}$ denote the pushout $( \Delta ^1 \times \operatorname{\mathcal{E}}_0) \coprod _{ ( \{ 1\} \times \operatorname{\mathcal{E}}_0 ) } \operatorname{\mathcal{E}}_{1}$, so that we can identify $\widetilde{\operatorname{\mathcal{B}}}$ with a summand of the Kan complex

\[ \operatorname{Hom}_{\operatorname{\mathcal{QC}}}(\operatorname{\mathcal{D}}_0,\operatorname{\mathcal{D}}_1) \times _{ \operatorname{Fun}( \operatorname{\mathcal{M}}, \operatorname{\mathcal{QC}})^{\simeq } } \operatorname{Fun}( \operatorname{\mathcal{M}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )^{\simeq }. \]

Note that $h$ induces a categorical equivalence of simpicial sets $h^{+}: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{E}}$ (Corollary 5.2.4.2). We have a commutative diagram of Kan complexes

5.62
\begin{equation} \begin{gathered}\label{equation:universality-formulation} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}})^{\simeq } } \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )^{\simeq } \ar [d] \ar [r] & \operatorname{Hom}_{\operatorname{\mathcal{QC}}}( \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \ar [d] \\ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )^{\simeq } \ar [d]^{\circ h^{+}} \ar [r]^-{ V \circ } & \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}})^{\simeq } \ar [d]^-{ \circ h^{+}} \\ \operatorname{Fun}( \operatorname{\mathcal{M}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )^{\simeq } \ar [r]^-{ V \circ } & \operatorname{Fun}( \operatorname{\mathcal{M}}, \operatorname{\mathcal{QC}})^{\simeq }, } \end{gathered} \end{equation}

where the upper vertical are homotopy equivalences (since $h^{+}$ is a categorical equivalence) and the horizontal maps are Kan fibrations (Corollary 4.4.5.7). Note that the top and bottom squares of (5.62) are homotopy pullback squares (Example 3.4.1.3 and Corollary 3.4.1.5). It follows that the outer rectangle is also a homotopy pullback square (Proposition 3.4.1.11): that is, precomposition with $h^{+}$ induces a homotopy equivalence of Kan complexes

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{\mathcal{QC}}}(\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}})^{\simeq } } \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )^{\simeq } \ar [d]^{ \varphi } \\ \operatorname{Hom}_{\operatorname{\mathcal{QC}}}(\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1) \times _{ \operatorname{Fun}( \operatorname{\mathcal{M}}, \operatorname{\mathcal{QC}})^{\simeq } } \operatorname{Fun}( \operatorname{\mathcal{M}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )^{\simeq }. } \]

Applying Remark 5.6.5.3, we see that $\operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^1)_{\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1}$ can be identified with the inverse image of $\widetilde{\operatorname{\mathcal{B}}}$ under the homotopy equivalence $\varphi $. In particular, $\varphi $ restricts to a homotopy equivalence $\varphi _0: \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^1 )_{ \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1} \rightarrow \widetilde{\operatorname{\mathcal{B}}}$. Unwinding the definitions, we see that the morphism

\[ \theta _{\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1}: \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^1 )_{ \operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1} \rightarrow \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Equiv}( \operatorname{\mathcal{E}}_{1}, \operatorname{\mathcal{E}}'_{1}) \]

coincides with the the composition $( \widetilde{r}_0, \widetilde{r}_1 ) \circ \varphi _0$. Since $( \widetilde{r}_0, \widetilde{r}_1)$ is a pullback of the trivial Kan fibration $(r_0, r_1): \operatorname{\mathcal{B}}\rightarrow \operatorname{Equiv}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{0} ) \times \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_{1} )^{\simeq }$, it is also a trivial Kan fibration. In a particular, $( \widetilde{r}_0, \widetilde{r}_1 )$ is a homotopy equivalence, so that the composite map $\theta _{\operatorname{\mathcal{D}}_0, \operatorname{\mathcal{D}}_1} = ( \widetilde{r}_0, \widetilde{r}_1 ) \circ \varphi _0$ is also a homotopy equivalence, as desired. $\square$