$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 7.5.3.2. Let $\operatorname{\mathcal{C}}$ be a small category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a cocartesian fibration of $\infty $-categories. Then the strict transport representation
\[ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Set_{\Delta }}\quad \quad C \mapsto \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ), \operatorname{\mathcal{E}}) \]
of Construction 5.3.1.5 is an isofibrant diagram of simplicial sets.
Proof.
Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Set_{\Delta }}$ be a functor and let $\mathscr {F}_0 \subseteq \mathscr {F}$ be a subfunctor for which the inclusion $\mathscr {F}_0 \hookrightarrow \mathscr {F}$ is a levelwise categorical equivalence. Suppose we are given a natural transformation $\alpha _0: \mathscr {F}_0 \rightarrow \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$. It follows from Proposition 7.5.3.1 that $\alpha _0$ can be extended to a natural transformation $\alpha : \mathscr {F} \rightarrow \operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$. To complete the proof, it will suffice to show that $\alpha $ factors through the subfunctor $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$. Equivalently, we must show that for each object $C \in \operatorname{\mathcal{C}}$, the lifting problem
\[ \xymatrix@R =50pt@C=50pt{ \mathscr {F}_0(C) \ar [r] \ar [d] & \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \ar [d] \\ \mathscr {F}(C) \ar [r] \ar@ {-->}[ur] & \operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) } \]
admits a (unique) solution. This is clear, since the left vertical map is a categorical equivalence and $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ is a replete subcategory of $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ (see Remark 5.3.1.15).
$\square$