Corollary 7.4.1.9. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of small simplicial sets and let $\operatorname{Tr}_{ \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be a covariant transport representation for $U$. Then the diagram $\operatorname{Tr}_{ \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}}$ 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. Using Proposition 7.4.1.6 (and Remark 7.4.1.7), we see that there exists a pullback diagram of small simplicial sets
\[ \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 a trivial Kan fibration. Using Corollary 5.6.5.11, we can extend $\operatorname{Tr}_{ \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}}$ to a diagram $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ which is a covariant transport representation for $\overline{U}$. Let ${\bf 0}$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleleft }$. It follows from Theorem 7.4.1.1 that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$, and therefore exhibits the $\infty $-category $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }( {\bf 0} ) \simeq \overline{\operatorname{\mathcal{E}}}_{ {\bf 0} }$ as a limit of the diagram $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$. Using Remark 7.4.1.5, we see that covariant diffraction supplies an equivalence of $\infty $-categories $\overline{\operatorname{\mathcal{E}}}_{ {\bf 0} } \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$, so that $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is also a limit of the diagram $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ (Proposition 7.1.1.12). $\square$