Kerodon

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

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

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, or alternatively that it is a homotopy equivalence (see Proposition 3.2.7.2).

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

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

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

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

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

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

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

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

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

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.6).

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

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

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

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.63) 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

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

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$

Proof. It follows from Lemma 5.6.8.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

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

Since the $1$-simplex $\Delta ^1$ is contractible (Example 3.2.4.2), 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.9.1. $\square$

Proof of Theorem 5.6.8.3. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially small cocartesian fibration of simplicial sets. 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

where each of the transition maps is a Kan fibration (Lemma 5.6.8.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.4.12 supplies a pushout diagram of simplicial sets

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

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.8.10), this is equivalent to the assertion that $\theta _0$ is a homotopy equivalence (Proposition 3.2.7.2). 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.9.2.

• In the case $k=1$, Lemma 5.6.9.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.8.10). Our inductive hypothesis guarantees that the Kan complex $X( \Lambda ^{k}_{i} )$ is contractible, so that $X( \Delta ^{k} )$ is also contractible.