# Kerodon

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

Corollary 5.6.2.11. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets and let $\mathscr {F}_0, \mathscr {F}_1: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be covariant transport representations for $U$. Then $\mathscr {F}_0$ and $\mathscr {F}_1$ are isomorphic as objects of the $\infty$-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$.

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.2.9, 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 S} = \mathscr {F}_0$ and $\mathscr {F}|_{ \{ 1\} \times S} = \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.2.6 (and Remark 5.2.7.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$