# Kerodon

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

Corollary 7.4.5.2. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration between small simplicial sets and let $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be a covariant transport representation for $U$. Then the simplicial set $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ of sections of $U$ is a Kan complex, which is a limit of the diagram $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ in the $\infty$-category $\operatorname{\mathcal{S}}$.

Proof. Since $U$ is a left fibration, Corollary 4.4.2.4 guarantees that the simplicial set $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is a Kan complex. Note that every edge of $\operatorname{\mathcal{E}}$ is $U$-cocartesian (Example 5.1.1.3), so that $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ coincides with the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ of cocartesian sections of $U$. Applying Corollary 7.4.1.9, we see that the Kan complex $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is a limit of the diagram $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ in the $\infty$-category $\operatorname{\mathcal{QC}}$, and therefore also in the full subcategory $\operatorname{\mathcal{S}}\subseteq \operatorname{\mathcal{QC}}$ (Proposition 7.4.5.1). $\square$