Proposition 7.4.1.6. Let $\operatorname{\mathcal{C}}$ be a small simplicial set and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be the covariant transport representation of a left fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ (Definition 5.6.5.1). Then the simplicial set $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is a Kan complex, which is a limit of the diagram $\mathscr {F}$.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof of Proposition 7.4.1.6. Let $\operatorname{\mathcal{C}}$ be a small simplicial set and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be the covariant transport representation of a left fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. Combining Propositions 7.4.1.9 and Proposition 7.4.1.14, we deduce that the Kan complex $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is homotopy equivalent to the morphism space $\operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}) }( \underline{ \Delta ^{0} }_{\operatorname{\mathcal{C}}}, \mathscr {F} )$ and is therefore a limit of $\mathscr {F}$ in the $\infty $-category $\operatorname{\mathcal{S}}$ (Corollary 7.4.1.2). $\square$