Kerodon

Proof. If $F$ is an equivalence of $\infty $-categories, then it carries initial objects to initial objects by virtue of Corollary 4.6.7.20. Conversely, suppose that $F( \widetilde{X} )$ is an initial object of $\operatorname{\mathcal{E}}$; we wish to show that $F$ is an equivalence of $\infty $-categories. Set $X = U( \widetilde{X} )$. Applying Proposition 5.6.6.19, we deduce that there is a functor $G \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$ such that $(G \circ F)( \widetilde{X} )$ is isomorphic to $\widetilde{X}$ as an object of the $\infty $-category $\operatorname{\mathcal{D}}_{X} = \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$. Applying Proposition 5.6.6.19 again, we deduce that $G \circ F$ is isomorphic to $\operatorname{id}_{\operatorname{\mathcal{D}}}$ as an object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{D}})$; in particular, $F$ is a right homotopy inverse to $G$. Since $G$ carries $F( \widetilde{X} )$ to an initial object of $\operatorname{\mathcal{D}}$, we can apply the same argument (with the roles of $\operatorname{\mathcal{D}}$ and $\operatorname{\mathcal{E}}$ reversed) to show that $G$ has a left homotopy inverse. It follows that $G$ is an equivalence of $\infty $-categories, so that $F$ is also an equivalence of $\infty $-categories. $\square$