Proposition 7.4.4.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of small simplicial sets and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be a covariant transport representation for $U$. Then the diagram $\mathscr {F}$ has a limit in the $\infty $-category $\operatorname{\mathcal{QC}}$, given by the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ of cocartesian sections of $U$.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof of Proposition 7.4.4.1. Let $\operatorname{\mathcal{C}}$ be a small simplicial set and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be the covariant transport representation for a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. Using Proposition 7.4.4.12, we can choose a pullback diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleleft }, } \]
where $\overline{U}$ is a cocartesian fibration and the restriction map
\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \]
is an equivalence of $\infty $-categories. It follows from Remark 7.4.4.13 that the cocartesian fibration $\overline{U}$ is essentially small, so that $\mathscr {F}$ admits an extension $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ which is a covariant transport representation for $\overline{U}$ (Corollary 5.6.5.13). Applying Theorem 7.4.4.6, we see that $\overline{\mathscr {F}}$ is a limit diagram in $\operatorname{\mathcal{QC}}$. In particular, it carries the cone point of $\operatorname{\mathcal{C}}^{\triangleleft }$ to an $\infty $-category $\operatorname{\mathcal{D}}$ which is a limit of the diagram $\mathscr {F}$. By virtue of Remark 7.4.4.11, the $\infty $-category $\operatorname{\mathcal{D}}$ is equivalent to the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ of cocartesian sections of $U$. $\square$