# Kerodon

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

Proposition 5.4.8.7. Let $\kappa$ be an uncountable regular cardinal and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty$-categories. Assume that $\operatorname{\mathcal{C}}$ is locally $\kappa$-small and that, for each object $C \in \operatorname{\mathcal{C}}$, the fiber $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is locally $\kappa$-small. Then $\operatorname{\mathcal{E}}$ is locally $\kappa$-small.

Proof. Let $X$ and $Y$ be objects of $\operatorname{\mathcal{E}}$, and set $\overline{X} = U(X)$ and $\overline{Y} = U(Y)$. We wish to show that the Kan complex $\operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y)$ is essentially $\kappa$-small. By virtue of Proposition 4.6.1.19, the functor $U$ induces a Kan fibration $\theta : \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}( \overline{X}, \overline{Y} )$. Our assumption that $\operatorname{\mathcal{C}}$ is locally $\kappa$-small guarantees that the Kan complex $\operatorname{Hom}_{\operatorname{\mathcal{C}}}( \overline{X}, \overline{Y} )$ is essentially $\kappa$-small. By virtue of Corollary 5.4.7.2, it will suffice to show that for every morphism $\overline{e}: \overline{X} \rightarrow \overline{Y}$ in $\operatorname{\mathcal{C}}$, the Kan complex $\operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y)_{\overline{e}} = \{ \overline{e} \} \times _{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}( \overline{X}, \overline{Y} ) } \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y)$ is essentially $\kappa$-small. Since $U$ is a cocartesian fibration, we can lift $\overline{e}$ to a $U$-cocartesian morphism $e: X \rightarrow Y'$ of $\operatorname{\mathcal{E}}$. Proposition 5.1.3.11 then supplies a homotopy equivalence of $\operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y)_{\overline{e}}$ with the mapping space $\operatorname{Hom}_{ \operatorname{\mathcal{E}}_{ \overline{Y} } }( Y', Y )$ which is essentially $\kappa$-small by virtue of our assumption that $\operatorname{\mathcal{E}}_{ \overline{Y} }$ is locally $\kappa$-small. $\square$