Kerodon

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

Corollary 7.1.4.12 (Uniqueness). Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories and let $X$ and $Y$ be $U$-initial objects of $\operatorname{\mathcal{C}}$. Then $X$ and $Y$ are isomorphic if and only if $U(X)$ and $U(Y)$ are isomorphic as objects of $\operatorname{\mathcal{D}}$.

Proof. Assume that there exists an isomorphism $\overline{f}: U(X) \rightarrow U(Y)$ in the $\infty $-category $\operatorname{\mathcal{D}}$. Since $X$ is $U$-initial, the functor $U$ induces a homotopy equivalence $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( U(X), U(Y) )$. It follows that there exists a morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$ such that $U(f)$ is homotopic to $\overline{f}$. In particular, $U(f): U(X) \rightarrow U(Y)$ is also an isomorphism in $\operatorname{\mathcal{D}}$. Applying Proposition 7.1.4.10, we deduce that $f$ is an isomorphism. In particular, the objects $X$ and $Y$ are isomorphic. $\square$