Kerodon

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

Proposition 10.2.3.15. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: X_0 \rightarrow X$ be a morphism of $\operatorname{\mathcal{C}}$. Then $f$ is a monomorphism if and only if it is subterminal when viewed as an object of the $\infty $-category $\operatorname{\mathcal{C}}_{/X}$.

Proof. By virtue of Proposition 10.2.3.14, the morphism $f$ is a monomorphism if and only if, for every object $C \in \operatorname{\mathcal{C}}$, every homotopy fiber of the composition map $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,X_0) \xrightarrow { [f] \circ } \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,X)$ is either empty or contractible. For every vertex $g \in \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,X)$, Corollary 4.6.9.18 identifies the corresponding homotopy fiber with the morphism space $\operatorname{Hom}_{\operatorname{\mathcal{C}}_{/X}}( g, f )$. The desired result now follows by allowing $g$ to vary. $\square$