5.4. The internalization of a small fibration [000Z]

Let $C$ be a small cartesian fibration (Definition 5·a [001Q]) over $B$ a category with finite limits, i.e. a cartesian fibration that is both locally small (Definition 4.1.3·b [001B]) and globally small (Definition 4.2·b [000P]). We will show that $C$ is equivalent to the externalization [000V] of an internal category [000O] $\underline{C}$ in $B$, namely the full internal subcategory [0011] associated to the generic object $\bar{u}\in C$.

By Theorem 5.3·a [001S] we know that the externalization of $\underline{C}$ so-defined is equivalent to the full subfibration $\FullSubfib{\bar{u}}$ of $C$ spanned by objects that are “classified” by $\bar{u}$. Because $\bar{u}$ is generic, we know that every object of $C$ is classified by $\bar{u}$, so we are done.