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

Remark (Uniqueness). Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories. Then, for every integer $n$, the factorization of Theorem is well-defined up to equivalence. More precisely, if the functor $F$ admits two factorizations

\[ \operatorname{\mathcal{C}}\xrightarrow {F'_0} \operatorname{\mathcal{D}}'_0 \xrightarrow {G_0} \operatorname{\mathcal{D}}\quad \quad \operatorname{\mathcal{C}}\xrightarrow {F'_1} \operatorname{\mathcal{D}}'_1 \xrightarrow {G_1} \operatorname{\mathcal{D}} \]

where the functors $F'_0$ and $F'_1$ are essentially $n$-categorical, and the functors $G_0$ are $G_1$ are categorically $(n+1)$-connective, then we can find a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^-{F'_0} & \operatorname{\mathcal{D}}'_0 \ar [r]^-{ G_0 } & \operatorname{\mathcal{D}}\\ \operatorname{\mathcal{C}}\ar@ {=}[u] \ar@ {=}[d] \ar [r] & \operatorname{\mathcal{D}}'_{01} \ar [u]_{\sim } \ar [d]^{\sim } \ar [r] & \operatorname{\mathcal{D}}\ar@ {=}[u] \ar@ {=}[d] \\ \operatorname{\mathcal{C}}\ar [r]^-{ F'_1 } & \operatorname{\mathcal{D}}'_{1} \ar [r]^-{ G_1 } & \operatorname{\mathcal{D}}} \]

where the vertical maps are equivalences of $\infty $-categories. To prove this, we can use Corollary to reduce to the case where $F'_0$ is a monomorphism of simplicial sets and $G_1$ is an isofibration. In this case, Corollary (and Remark guarantee that the functors $F'_0$ and $G_1$ induce a trivial Kan fibration

\[ \operatorname{Fun}( \operatorname{\mathcal{D}}'_0, \operatorname{\mathcal{D}}'_1 ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}'_1 ) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) } \operatorname{Fun}( \operatorname{\mathcal{D}}'_0, \operatorname{\mathcal{D}}). \]

In particular, this map is surjective on vertices, so the lifting problem

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^-{F'_1} \ar [d]^{F'_0} & \operatorname{\mathcal{D}}'_1 \ar [d]^{G_1} \\ \operatorname{\mathcal{D}}'_0 \ar [r]^-{G_0} \ar@ {-->}[ur] & \operatorname{\mathcal{D}}} \]

has a solution. A choice of solution determines a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^-{F'_0} \ar@ {=}[d] & \operatorname{\mathcal{D}}'_0 \ar [r]^-{ G_0 } \ar [d]^{H} & \operatorname{\mathcal{D}}\ar@ {=}[d] \\ \operatorname{\mathcal{C}}\ar [r]^-{ F'_1 } & \operatorname{\mathcal{D}}'_{1} \ar [r]^-{ G_1 } & \operatorname{\mathcal{D}}. } \]

It follows from Proposition that the functor $H$ is categorically $(n+1)$-connective, and from Remark that $H$ is essentially $n$-categorical. Applying Remark, we conclude that $H$ is an equivalence of $\infty $-categories.