# Kerodon

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

Lemma 5.6.8.7. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Then the simplicial set $\operatorname{TW}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ is a Kan complex.

Proof. Since $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is an $\infty$-category (Lemma 5.6.8.6), it will suffice to show that every morphism $u$ of $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is an isomorphism (Proposition 4.4.2.1). Let us identify $u$ with a commutative diagram of simplicial sets

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

satisfying conditions $(a)$ and $(b)$ of Remark 5.6.5.3.

Passing to homotopy categories, we see that $\mathscr {F}$ induces a functor $\mathrm{h} \mathit{\mathscr {F}}: [1] \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{\mathcal{QC}}} \simeq \mathrm{h} \mathit{\operatorname{QCat}}$. Applying Remark 5.6.5.8, we see that $\mathrm{h} \mathit{\mathscr {F}}$ is isomorphic to the composite functor $[1] \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \twoheadrightarrow \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \xrightarrow { \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} } \mathrm{h} \mathit{\operatorname{QCat}}$, where $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ denotes the homotopy transport representation of Construction 5.2.5.2. It follows that, for every vertex $C \in \operatorname{\mathcal{C}}$, the morphism $\mathscr {F}$ carries the edge $\Delta ^1 \times \{ C\}$ to an isomorphism $\overline{e}$ in $\operatorname{\mathcal{QC}}$. If $X$ is an object of $\operatorname{\mathcal{E}}$ satisfying $U(X) = C$, then $\widetilde{\mathscr {F}}$ carries $\Delta ^1 \times \{ X\}$ to a $V$-cocartesian morphism $e$ of $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$ satisfying $V(e) = \overline{e}$, which is then also an isomorphism by virtue of Corollary 5.1.1.10. Allowing $C$ and $X$ to vary and applying Theorem 4.4.4.4, we deduce that $\mathscr {F}$ and $\widetilde{\mathscr {F}}$ are isomorphisms when regarded as morphisms in the $\infty$-categories $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$ and $\operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )$, respectively.

Set $\operatorname{\mathcal{M}}= \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}) } \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}})$. Applying Corollary 4.4.3.19 to the pullback diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{M}}\ar [r] \ar [d] & \operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \ar [d] \\ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}}) \ar [r] & \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}), }$

we deduce that $u$ is an isomorphism when regarded as a morphism of the $\infty$-category $\operatorname{\mathcal{M}}$. Since $\operatorname{TW}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ is replete subcategory of $\operatorname{\mathcal{M}}$ (Lemma 5.6.8.6), it follows that $u$ is also an isomorphism when regarded as a morphism of $\operatorname{TW}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ (Example 4.4.2.9). $\square$