Kerodon

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

Proposition 7.4.2.6. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ be a natural transformation between functors $\mathscr {F}, \mathscr {F}': \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ which are given as covariant transport representations for left fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$, respectively. Then there exists a morphism $\Gamma \in \operatorname{Hom}_{ \operatorname{LFib}(\operatorname{\mathcal{C}}) }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' )$ which is compatible with $\gamma $. Moreover, the homotopy class $[\Gamma ]$ is uniquely determined.

Proof. Fix natural transformations $\alpha : \underline{\Delta ^0}_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ and $\alpha ': \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}'|_{\operatorname{\mathcal{E}}'}$ which exhibit $\mathscr {F}$ and $\mathscr {F}'$ are covariant transport representations for $U$ and $U'$, respectively. Then $\alpha '$ induces a map of Kan complexes

7.50
\begin{eqnarray} \label{equation:induced-map-of-covariant-transport} \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) & \xrightarrow {\rho } & \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{S}}) }( \underline{\Delta ^0}_{\operatorname{\mathcal{E}}}, \mathscr {F}'|_{\operatorname{\mathcal{E}}} ), \end{eqnarray}

which carries a morphism $\Gamma \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' )$ to the pullback of $\alpha '$ along $\Gamma $. To prove Proposition 7.4.2.6, it suffices to show that $\rho $ is bijective on connected components. In fact, the morphism $\rho $ is a homotopy equivalence: this follows by applying Proposition 7.4.1.14 to the left fibration $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$. $\square$