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
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.10, 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.11. 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
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$