Kerodon

Proof. Fix an object $G$ of the $\infty $-category $\operatorname{\mathcal{M}}= \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{\mathcal{E}})$. We wish to show that the Kan complex $X = \operatorname{Hom}_{\operatorname{\mathcal{M}}}(F,G)$ is contractible. For every morphism of simplicial sets $S \rightarrow \operatorname{\mathcal{C}}$, set $\operatorname{\mathcal{M}}_{S} = \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(S), \operatorname{\mathcal{E}})$, let $F_{S}$ and $G_{S}$ denote the images of $F$ and $G$ in the $\infty $-category $\operatorname{\mathcal{M}}_{S}$, and let $X_ S$ denote the Kan complex $\operatorname{Hom}_{ \operatorname{\mathcal{M}}_{S} }( F_ S, G_ S )$. Let us say that $S$ is good if the Kan complex $X_{S}$ is contractible. We will complete the proof by showing that every object $S \in (\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$ is good. We make the following observations:

$(i)$

Since the functor $S \mapsto \operatorname{Tw}(S)$ commutes with colimits (Remark 8.1.1.4), the construction $S \mapsto \operatorname{\mathcal{M}}_{S}$ carries colimits (in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$) to limits (in the category of simplicial sets). It follows that the construction $S \mapsto X_{S}$ has the same property.

$(ii)$

Let $S' \hookrightarrow S$ be a monomorphism in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$. Then the induced map $\operatorname{Tw}(S') \rightarrow \operatorname{Tw}(S)$ is also a monomorphism, so the restriction map $\operatorname{\mathcal{M}}_{S} \rightarrow \operatorname{\mathcal{M}}_{S'}$ is an isofibration of $\infty $-categories (Proposition 4.5.5.14). It follows that the induced map $X_{S} \rightarrow X_{S'}$ is a Kan fibration (Proposition 4.6.1.21).

Let $S \rightarrow \operatorname{\mathcal{C}}$ be any morphism of simplicial sets. Using $(i)$ and $(ii)$, we see that $X_{S}$ can be realized as the limit of a tower of Kan fibrations

Consequently, to show that $S$ is good, it will suffice to show that each skeleton $\operatorname{sk}_ n(S)$ is good (Example 4.5.6.18). Replacing $S$ by $\operatorname{sk}_{n}(S)$, we can reduce to the case where $S$ has dimension $\leq n$, for some integer $n \geq -1$.

We now proceed by induction on $n$. If $n= -1$, then the simplicial set $S$ is empty and the Kan complex $X_{S}$ is isomorphic to $\Delta ^0$ (by virtue of $(i)$). Let us therefore assume that $n \geq 0$. Let $T$ denote the coproduct $\coprod _{\sigma } \Delta ^ n$, indexed by the collection of nondegenerate $n$-simplices of $S$, so that Proposition 1.1.4.12 supplies a pushout diagram of simplicial sets

Applying $(i)$, we obtain a pullback diagram of Kan complexes

It follows from $(ii)$ that the vertical maps in this diagram are Kan fibrations, so that (11.15) is a homotopy pullback diagram (Example 3.4.1.3). Our inductive hypothesis guarantees that the Kan complexes $X_{ \operatorname{sk}_{n-1}(S) }$ and $X_{ \operatorname{sk}_{n-1}(T) }$ are contractible, so that the lower horizontal map is a homotopy equivalence. Applying Corollary 3.4.1.5, we see that the map $X_{S} \rightarrow X_{T}$ is also a homotopy equivalence. We may therefore replace $S$ by $T$, and thereby reduce to the case where $S$ is a coproduct of simplices. Since the collection of contractible Kan complexes is closed under the formation of products (Remark 3.1.6.8), we can use $(i)$ to further reduce to the special case where $S = \Delta ^ n$ is a standard simplex. Replacing $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ by the projection map $S \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow S$, we are reduced to proving Lemma 11.9.3.6 in the special case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex.

Let us identify the twisted arrow $\infty $-category $\operatorname{Tw}(\operatorname{\mathcal{C}})$ with the nerve of the partially ordered set $Q = \{ (i,j) \in [n]^{\operatorname{op}} \times [n]: i \leq j \} $, so that $F$ and $G$ can be identified with functors from $\operatorname{N}_{\bullet }(Q)$ into $\operatorname{\mathcal{E}}$. Let $Q' \subset Q$ be as in Remark 11.9.3.5, so that $F$ is $U$-left Kan extended from $\operatorname{N}_{\bullet }(Q')$. Set $\operatorname{\mathcal{M}}' = \operatorname{Fun}_{ / \Delta ^ n}( \operatorname{N}_{\bullet }(Q'), \operatorname{\mathcal{E}})$, so that the restriction map

is a homotopy equivalence (Proposition 7.3.6.7). It will therefore suffice to show that the mapping space $\operatorname{Hom}_{ \operatorname{\mathcal{M}}' }( F|_{ \operatorname{N}_{\bullet }(Q') }, G|_{ \operatorname{N}_{\bullet }(Q') })$, which follows from our inductive hypothesis (applied to the inclusion map $\Delta ^{n-1} \hookrightarrow \Delta ^{n}$). $\square$