# Kerodon

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

Remark 4.8.8.8 (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 4.8.8.3 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 4.5.2.23 to reduce to the case where $F'_0$ is a monomorphism of simplicial sets and $G_1$ is an isofibration. In this case, Corollary 4.8.7.18 (and Remark 4.8.7.19) 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 4.8.7.12 that the functor $H$ is categorically $(n+1)$-connective, and from Remark 4.8.6.7 that $H$ is essentially $n$-categorical. Applying Remark 4.8.5.11, we conclude that $H$ is an equivalence of $\infty$-categories.