Kerodon

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

Corollary 8.4.0.43. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a cartesian fibration of $\infty $-categories and let $C$ be an object of $\operatorname{\mathcal{C}}$ whose image $D = F(C)$ is an initial object of $\operatorname{\mathcal{D}}$. Then $C$ is an initial object of $\operatorname{\mathcal{C}}$ if and only if it is an initial object of the fiber $\operatorname{\mathcal{C}}_{D} = \{ D\} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}$.