Lemma 4.7.6.11. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an equivalence of $\infty $-categories. If $\operatorname{\mathcal{C}}$ is minimal, then $F$ is a monomorphism of simplicial sets.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Let $\sigma , \sigma ': \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ be $n$-simplices of $\operatorname{\mathcal{C}}$ satisfying $F(\sigma ) = F(\sigma ')$; we wish to show that $\sigma = \sigma '$. Our proof proceeds by induction on $n$. Set $\tau = F(\sigma ) = F(\sigma ')$ and $\sigma _0 = \sigma |_{ \operatorname{\partial \Delta }^ n }$, so that our inductive hypothesis guarantees that $\sigma _0 = \sigma '|_{ \operatorname{\partial \Delta }^ n}$.
Fix a functor $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ which is homotopy inverse to $F$, so that there exists a $2$-simplex
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{id}_{ \operatorname{\mathcal{C}}} \ar [rr]^-{ \operatorname{id}} \ar [dr]_{\alpha } & & \operatorname{id}_{ \operatorname{\mathcal{C}}} \\ & G \circ F \ar [ur]_{\beta } & } \]
in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{C}})$, where $\alpha $ and $\beta $ are (mutually inverse) isomorphisms. Precomposing with the morphism $\sigma _0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{C}}$, we obtain a $2$-simplex
4.76
\begin{equation} \begin{gathered}\label{equation:minimal-is-mono} \xymatrix@R =50pt@C=50pt{ \sigma _0 \ar [rr]^-{ \operatorname{id}} \ar [dr]_{\alpha (\sigma _0)} & & \sigma _0 \\ & (G \circ F)(\sigma _0) \ar [ur]_{\beta (\sigma _0)} & } \end{gathered} \end{equation}
in the $\infty $-category $\operatorname{Fun}( \operatorname{\partial \Delta }^ n, \operatorname{\mathcal{C}})$. Since $\operatorname{\mathcal{C}}$ is an $\infty $-category, Theorem 1.5.6.1 guarantees that we can lift (4.76) to a $2$-simplex
\[ \xymatrix@R =50pt@C=50pt{ \sigma \ar [rr]^-{ \gamma } \ar [dr]_{\alpha (\sigma )} & & \sigma ' \\ & G(\tau ). \ar [ur]_{\beta (\sigma ')} & } \]
in the $\infty $-category $\operatorname{Fun}( \Delta ^ n, \operatorname{\mathcal{C}})$. By construction, $\gamma $ is an isomorphism relative to $\operatorname{\partial \Delta }^ n$. Invoking our assumption that $\operatorname{\mathcal{C}}$ is minimal, we deduce that $\sigma = \sigma '$. $\square$