Kerodon

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

Example 7.4.1.12. Let $\operatorname{\mathcal{C}}= \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}_0)$ be the nerve of a category $\operatorname{\mathcal{C}}_0$, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration of $\infty $-categories, and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ denote the (homotopy coherent) nerve of the strict transport representation $\mathscr {F}_0 = \operatorname{sTr}_{\operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}_0}$ (see Construction 5.3.1.5). Set $\operatorname{\mathcal{E}}' = \operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}}_0)$, so that Example 7.4.1.11 supplies a natural transformation $\alpha ': \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}'} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}'}$ which exhibits $\mathscr {F}$ as a covariant transport representation of $U'$. The scaffolds of Constructions 5.3.4.7 and 5.3.4.11 provide categorical equivalences of simplicial sets

\[ \operatorname{\mathcal{E}}\xleftarrow { \lambda _{u} } \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F}_0 ) \xrightarrow { \lambda _{t} } \operatorname{\mathcal{E}}'. \]

It follows that there exists a natural transformation $\alpha : \underline{\Delta ^0}_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ which is characterized up to homotopy by the requirement that $[\alpha ]$ and $[\alpha ']$ have the same image in the homotopy category $\mathrm{h} \mathit{ \operatorname{Fun}( \underset { \longrightarrow }{\mathrm{holim}}(\mathscr {F}_0), \operatorname{\mathcal{S}})}$. Moreover, $\alpha $ exhibits $\mathscr {F}$ as a covariant transport representation for $U$. Beware that, although the homotopy class $[\alpha ]$ is canonically determined, the construction of $\alpha $ requires some auxiliary choices (which cannot be made functorially at the level of simplicial sets).