Kerodon

Proof. Let $\operatorname{Ret}$ denote the category introduced in Construction 8.5.0.2. Using Proposition 8.5.6.10, we can choose a functor $F: \operatorname{N}_{\bullet }(\operatorname{Ret}) \rightarrow \operatorname{\mathcal{C}}$ satisfying $F(\widetilde{X} ) = X$ and $F( \widetilde{e} )= e$.

Let $Q: \operatorname{Spine}[\operatorname{\mathbf{Z}}] \rightarrow \operatorname{N}_{\bullet }( \operatorname{Idem})$ denote the (left and right) cofinal morphism of Proposition 8.5.4.16, and let $Q^{-}: \operatorname{Spine}[\operatorname{\mathbf{Z}}]^{\triangleleft } \rightarrow \operatorname{N}_{\bullet }(\operatorname{Ret})$ and $Q^{+}: \operatorname{Spine}[\operatorname{\mathbf{Z}}]^{\triangleright } \rightarrow \operatorname{N}_{\bullet }( \operatorname{Ret})$ be the extensions of Notation 8.5.6.15. Lemma 8.5.6.16 guarantees that $F \circ Q^{-}$ is a limit diagram in $\operatorname{\mathcal{C}}$ extending $F \circ Q = T_{e}$, so that $e$ satisfies condition $(1)$ of Definition 8.5.6.14. Similarly, $F \circ Q^{+}$ is a colimit diagram extending $T_{e}$, so that $e$ satisfies condition $(2)$ of Definition 8.5.6.14. Condition $(3)$ follows from the observation that any composition of $F( \widetilde{i} )$ with $F( \widetilde{r} )$ is homotopic to the morphism $F( \widetilde{r} \circ \widetilde{i} ) = F( \operatorname{id}_{ \widetilde{Y} } ) = \operatorname{id}_{ F( \widetilde{Y} ) }$, and is therefore an isomorphism. $\square$