Kerodon

Proof. Since $\operatorname{\mathcal{C}}$ is essentially finite, we can choose a categorical equivalence $U_0: \operatorname{\mathcal{D}}_0 \rightarrow \operatorname{\mathcal{C}}$, where $\operatorname{\mathcal{D}}_0$ is a finite simplicial set. Arguing as in the proof of Proposition 4.1.3.2, we can factor $U_0$ as a composition $\operatorname{\mathcal{D}}_0 \xrightarrow {j} \operatorname{\mathcal{D}}\xrightarrow {U} \operatorname{\mathcal{C}}$, where $U$ is an inner fibration and $j$ is a transfinite composition of pushouts of inner horn inclusions. More precisely, we may assume that $\operatorname{\mathcal{D}}= \operatorname{\mathcal{D}}_{\beta }$ for some ordinal $\beta $ and some well-ordered diagram

having the following properties:

• For every ordinal $\alpha < \beta $, there is a pair of integers $0 < i < n$ and a pushout diagram of simplicial sets

  \[ \xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{i} \ar [r] \ar [d] & \operatorname{\mathcal{D}}_{\alpha } \ar [d] \\ \Delta ^{n} \ar [r]^{ \sigma _{\alpha } } & \operatorname{\mathcal{D}}_{\alpha +1}. } \]

  In what follows, we will identify $\sigma _{\alpha }$ with an $n$-simplex of $\operatorname{\mathcal{D}}$ and write $\tau _{\alpha }$ for its $i$th face $d^{n}_{i}( \sigma _{\alpha } )$.

• For every nonzero limit ordinal $\lambda \leq \beta $, the comparison map $\varinjlim _{\alpha < \lambda } \operatorname{\mathcal{D}}_{\alpha } \rightarrow \operatorname{\mathcal{D}}_{\lambda }$ is an isomorphism.

Let us say that a simplicial subset $S \subseteq \operatorname{\mathcal{D}}$ is saturated if, whenever $S$ contains the simplex $\tau _{\alpha }$, then it also contains the simplex $\sigma _{\alpha }$. If $S$ is any simplicial subset of $\operatorname{\mathcal{D}}$, then there is a smallest saturated simplicial subset $S^{+}$ which contains $S$. Moreover, if $S$ is finite, then $S^{+}$ is also finite.

Since $U$ is an inner fibration, $\operatorname{\mathcal{D}}$ is an $\infty $-category. Since $U_0$ and $j$ are categorical equivalences of simplicial sets, the functor $U$ is an equivalence of $\infty $-categories, and therefore admits a homotopy inverse $U^{-1}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$. Let $L \subseteq \operatorname{\mathcal{D}}$ be the smallest saturated simplicial subset which contains both $\operatorname{\mathcal{D}}_0$ and the image of the diagram $(U^{-1} \circ f_0): K_0 \rightarrow \operatorname{\mathcal{D}}$. For $\alpha \leq \beta $, set $L_{\alpha } = L \cap \operatorname{\mathcal{D}}_{\alpha }$. Then the inclusion map $\operatorname{\mathcal{D}}_0 = L_0 \hookrightarrow L_{\beta } = L$ can be realized as a transfinite composition of morphisms $L_{\alpha } \hookrightarrow L_{\alpha +1}$, each of which is either a pushout of an inner horn inclusion (if the simplex $\sigma _{\alpha }$ is contained in $L$) or an isomorphism (if $\sigma _{\alpha }$ is not contained in $L$). In particular, the inclusion $\operatorname{\mathcal{D}}_0 \hookrightarrow L$ is inner anodyne, so that $U|_{L}: L \rightarrow \operatorname{\mathcal{C}}$ is a categorical equivalence of simplicial sets.

By construction, the composition $U^{-1} \circ f_0$ can be regarded as a morphism of simplicial sets $g: K_0 \rightarrow L$. Set $f_{1} = U|_{L} \circ g$. Since $U^{-1}$ is a homotopy inverse to $U$, $f_0$ and $f_{1}$ are isomoprhic when regarded as objects of the $\infty $-category $\operatorname{Fun}(K, \operatorname{\mathcal{C}})$. Let $Q$ be a finite simplicial set equipped with a monomorphism $e: \Delta ^1 \hookrightarrow Q$ which exhibits $Q$ as a localization of $\Delta ^1$ with respect to its nondegenerate edge (for example, we can take $Q$ to be the quotient of $\Delta ^3$ appearing in Corollary 6.3.2.8). Let $q_0$ and $q_1$ be the vertices of $Q$ given by the source and target of the edge $e$. Our assumption that $f_0$ and $f_1$ are isomorphic is then equivalent to the assertion that there exists a diagram $h: Q \rightarrow \operatorname{Fun}(K_0, \operatorname{\mathcal{C}})$ satisfying $h(q_0) = f_0$ and $h(q_1) = f_1$. Let us identify $h$ with a morphism of simplicial sets $H: Q \times K_0 \rightarrow \operatorname{\mathcal{C}}$.

Note that the projection map $Q \rightarrow \Delta ^0$ is a categorical equivalence of simplicial sets (see Corollary 6.3.2.7), so the inclusion $\{ q_1 \} \hookrightarrow Q$ has the same property. Form a pushout diagram

so that the left vertical map determines a categorical equivalence $L \hookrightarrow K$ (Remark 4.5.4.13). By construction, there is a unique morphism of simplicial sets $f: K \rightarrow \operatorname{\mathcal{C}}$ satisfying $f|_{L} = U|_{L}$ and $f|_{ (Q \times K_0) } = H$. Since $U|_{L}$ is a categorical equivalence, it follows that $f$ is a categorical equivalence. We conclude by observing that $f_0$ can be recovered as the composition $f \circ u$, where $u$ is the monomorphism given by the composition