Kerodon

Proof of Theorem 2.4.5.1. Let $\operatorname{\mathcal{C}}_{\bullet }$ be a locally Kan simplicial category; we wish to show that the homotopy coherent nerve $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{\mathcal{C}})$ is an $\infty $-category. Fix positive integers $0 < i < n$; we wish to show that every map of simplicial sets $\sigma _0: \Lambda ^ n_ i \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{\mathcal{C}})$ can be extended to an $n$-simplex $\sigma : \Delta ^ n \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{\mathcal{C}})$. Let us identify $\sigma _0$ with a simplicial functor $F: \operatorname{Path}[ \Lambda ^{n}_{i} ]_{\bullet } \rightarrow \operatorname{\mathcal{C}}_{\bullet }$ inducing a map of simplicial sets $\lambda _0: {\boldsymbol {\sqcap }}^{n-1}_{i} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}( F(0), F(n) )_{\bullet }$. By virtue of Corollary 2.4.5.10, it will suffice to show that $\lambda _0$ can be extended to a map of simplicial sets $\lambda : \operatorname{\raise {0.1ex}{\square }}^{n-1} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}( F(0), F(n) )_{\bullet }$. The existence of this extension follows from Corollary 2.4.5.12, by virtue of our assumption that $\operatorname{Hom}_{\operatorname{\mathcal{C}}}( F(0), F(n) )_{\bullet }$ is a Kan complex. $\square$