Kerodon

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

5.6.6 Uniqueness of the Transport Representation

Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, and suppose that the fiber $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is essentially small for each vertex $C \in \operatorname{\mathcal{C}}$. Our goal in this section is to prove Theorem 5.6.5.3, which that the space of transport witnesses $\operatorname{TW}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ of Notation 5.6.5.1 is a contractible Kan complex. The main step is to establish the following:

Lemma 5.6.6.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 \coprod \operatorname{\mathcal{E}}_{1} / \operatorname{\partial \Delta }^{1} ) \]

is a trivial Kan fibration of simplicial sets.

Proof. It follows from Lemma 5.6.5.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.5.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 \coprod \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}}'_{X} ) \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.7.1). It follows from Proposition 5.4.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.4, 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.1). Form a pullback diagram

5.55
\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.5.2). We have a commutative diagram of Kan complexes

5.56
\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.56) are homotopy pullback squares (Example 3.4.1.5 and Corollary 3.4.1.3). It follows that the outer rectangle is also a homotopy pullback square (Proposition 3.4.1.9): that is, precomposition with $h^{+}$ induces a homotopy equivalence of Kan complexes

\[ \xymatrix { \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.2.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$

Lemma 5.6.6.2. Let $\operatorname{\mathcal{E}}$ be an essentially small $\infty $-category. Then the simplicial set $\operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^0 )$ is a contractible Kan complex.

Proof. It follows from Lemma 5.6.5.7 that the simplicial set $\operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^0 )$ is a Kan complex. Since $\operatorname{\mathcal{E}}$ is essentially small, the Kan complex $\operatorname{TW}(\operatorname{\mathcal{E}}/ \Delta ^0)$ is nonempty. It will therefore suffice to show that the diagonal map

\[ \delta : \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^0 ) \rightarrow \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^0 ) \times \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^0 ) \]

is a homotopy equivalence (Corollary 3.2.7.6). Unwinding the definitions, we see that $\delta $ factors as a composition

\begin{eqnarray*} \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^0 ) & \xrightarrow {\delta '} & \operatorname{Fun}( \Delta ^1, \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^0) ) \\ & \simeq & \operatorname{TW}( \Delta ^1 \times \operatorname{\mathcal{E}}/ \Delta ^1 ) \\ & \xrightarrow {\delta ''} & \operatorname{TW}( \operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{E}}/ \operatorname{\partial \Delta }^1 ) \\ & \simeq & \operatorname{TW}( \operatorname{\mathcal{E}}/ \Delta ^0 ) \times \operatorname{TW}(\operatorname{\mathcal{E}}/ \Delta ^0 ). \end{eqnarray*}

Since the $1$-simplex $\Delta ^1$ is contractible (Example 3.2.6.3), the morphism $\delta '$ is a homotopy equivalence. It will therefore suffice to show that the restriction map $\delta ''$ is a homotopy equivalence, which follows from Lemma 5.6.6.1. $\square$

Proof of Theorem 5.6.5.3. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Assume that, for each vertex $C \in \operatorname{\mathcal{C}}$, the $\infty $-category $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is essentially small. We wish to show that the simplicial set $\operatorname{TW}(\operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is a contractible Kan complex.

For every simplicial set $\operatorname{\mathcal{C}}_0$ equipped with a morphism $\operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$, let $X( \operatorname{\mathcal{C}}_0 )$ denote the simplicial set $\operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 )$, where $\operatorname{\mathcal{E}}_0$ is the fiber product $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Note that the simplicial set $X(\operatorname{\mathcal{C}}) = \operatorname{TW}(\operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ can be realized as the inverse limit of the tower

\[ \cdots \rightarrow X( \operatorname{sk}_{2}(\operatorname{\mathcal{C}}) ) \rightarrow X( \operatorname{sk}_{1}(\operatorname{\mathcal{C}}) ) \rightarrow X(\operatorname{sk}_{0}(\operatorname{\mathcal{C}}) ), \]

where each of the transition maps is a Kan fibration (Lemma 5.6.5.10). Consequently, to show that $X(\operatorname{\mathcal{C}})$ is a contractible Kan complex, it will suffice to show that each of the simplicial sets $X( \operatorname{sk}_{k}(\operatorname{\mathcal{C}}) )$ is a contractible Kan complex. Replacing $\operatorname{\mathcal{C}}$ by $\operatorname{sk}_{k}(\operatorname{\mathcal{C}})$, we can assume that the simplicial set $\operatorname{\mathcal{C}}$ has dimension $\leq k$, for some integer $k \geq -1$.

We now proceed by induction on $k$. In the case $k=-1$, the simplicial set $\operatorname{\mathcal{C}}$ is empty and $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is isomorphic to $\Delta ^0$. We may therefore assume without loss of generality that $k \geq 0$. Let $S$ be the collection of nondegenerate $k$-simplices of $\operatorname{\mathcal{C}}$, so that Proposition 1.1.3.13 supplies a pushout diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \underset { \sigma \in S }{\coprod } \operatorname{\partial \Delta }^{k} \ar [r] \ar [d] & \underset { \sigma \in S }{\coprod } \Delta ^{k} \ar [d] \\ \operatorname{\mathcal{C}}_0 \ar [r] & \operatorname{\mathcal{C}}, } \]

where $\operatorname{\mathcal{C}}_0 = \operatorname{sk}_{k-1}(\operatorname{\mathcal{C}})$ is the $(k-1)$-skeleton of $\operatorname{\mathcal{C}}$. It follows from our inductive hypothesis that the simplicial set $X(\operatorname{\mathcal{C}}_0)$ is a contractible Kan complex. Consequently, to show that $X(\operatorname{\mathcal{C}})$ is a contractible Kan complex, it will suffice to show that the restriction map $\theta : X(\operatorname{\mathcal{C}}) \rightarrow X(\operatorname{\mathcal{C}}_0)$ is a trivial Kan fibration. Note that $\theta $ is a pullback of the restriction map

\[ \theta _0: X( \underset { \sigma \in S }{\coprod } \Delta ^{k} ) \rightarrow X( \underset { \sigma \in S }{\coprod } \operatorname{\partial \Delta }^{k} ). \]

We will complete the proof by showing that $\theta _0$ is a trivial Kan fibration. Since $\theta _0$ is a Kan fibration (Lemma 5.6.5.10), this is equivalent to the assertion that $\theta _0$ is a homotopy equivalence (Corollary 3.2.7.4). Our inductive hypothesis guarantees that the Kan complex $X( \underset { \sigma \in S }{\coprod } \operatorname{\partial \Delta }^{k} )$ is contractible. We are therefore reduced to showing that the Kan complex $X( \underset { \sigma \in S }{\coprod } \Delta ^{k} )$ is also contractible. Since the collection of contractible Kan complexes is closed under products, we are reduced to verifying the contractibility of the simplicial set $X( \operatorname{\mathcal{C}}_0 )$ in the special case where $\operatorname{\mathcal{C}}_0 = \Delta ^{k}$ is a standard simplex of dimension $k$. We now consider several cases:

  • In the case $k=0$, the desired result follows from Lemma 5.6.6.2.

  • In the case $k=1$, Lemma 5.6.6.1 supplies a trivial Kan fibration $X( \Delta ^1 ) \rightarrow X( \operatorname{\partial \Delta }^1 )$. Our inductive hypothesis guarantees that the Kan complex $X( \operatorname{\partial \Delta }^1 )$ is contractible, so that $X( \Delta ^1)$ is also contractible.

  • In the case $k \geq 2$, we can choose an integer $0 < i < k$. In this case, the inclusion $\Lambda ^{k}_{i} \hookrightarrow \Delta ^{k}$ is inner anodyne, so the restriction map $X( \Delta ^{k} ) \rightarrow X( \Lambda ^{k}_{i} )$ is a trivial Kan fibration (Lemma 5.6.5.10). Our inductive hypothesis guarantees that the Kan complex $X( \Lambda ^{k}_{i} )$ is contractible, so that $X( \Delta ^{k} )$ is also contractible.

$\square$