Kerodon

Proof. Let $U_{\Delta ^1}: \Delta ^1 \times \operatorname{\mathcal{E}}\rightarrow \Delta ^1 \times \operatorname{\mathcal{C}}$ be the product of $U$ with the identity map $\operatorname{id}_{ \Delta ^1}$, and define $U_{\operatorname{\partial \Delta }^1}: \operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{E}}\rightarrow \operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{C}}$ similarly. Note that the map $( \mathscr {F}_0, \mathscr {F}_1 ): \operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ is a covariant transport representation of $U_{\operatorname{\partial \Delta }^1}$. Applying Corollary 5.6.5.13, we deduce that $U_{\Delta ^1}$ admits a covariant transport representation $\mathscr {F}: \Delta ^1 \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ which satisfies $\mathscr {F}|_{ \{ 0\} \times \operatorname{\mathcal{C}}} = \mathscr {F}_0$ and $\mathscr {F}|_{ \{ 1\} \times \operatorname{\mathcal{C}}} = \mathscr {F}_1$. Let us identify $\mathscr {F}$ with a morphism $u: \mathscr {F}_{0} \rightarrow \mathscr {F}_{1}$ in the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$. We will complete the proof by showing that $u$ is an isomorphism. By virtue of Theorem 4.4.4.4, it will suffice to show that for each vertex $C \in \operatorname{\mathcal{C}}$, the induced map $u_ C: \mathscr {F}_0(C) \rightarrow \mathscr {F}_1(C)$ is an isomorphism in $\operatorname{\mathcal{QC}}$. Using Remark 5.6.5.10 (and Remark 5.2.8.5), we see that the homotopy class $[u_ C]$ is isomorphic (as an object of the arrow category $\operatorname{Fun}( [1], \mathrm{h} \mathit{\operatorname{QCat}} )$) to the homotopy class of the functor $\operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C}$ given by covariant transport along the degenerate edge $\operatorname{id}_{C}$ of $\operatorname{\mathcal{C}}$: that is, the homotopy class of the identity functor $\operatorname{id}_{ \operatorname{\mathcal{E}}_{C} }$. $\square$