The density theorem in the ordinary category theory asserts that every presheaf on a small category is a colimit of representables in a canonical way. In Lemma 5.1.5.3 of *Higher Topos Theory*, Lurie proves an $\infty$-categorical version of this. There is a part of the proof which is not clear to me, and I hope someone kindly gives me an elaboration of the proof. (This question has already been asked previously on MSE [(see here)][1], but the question has not received an accepted answer yet. Given that it was asked about a year and a half ago, I decided that it wouldn't be inappropriate to ask the question again here.)

The lemma asserts the following: 
 > If $S$ is a simplicial set, then $\operatorname{id}_{\mathcal{P}(S)}$ is the left Kan extension of the Yoneda embedding $j:S\to\mathcal{P}(S)=\operatorname{Fun}(S^{\mathrm{op}},\mathcal{S})$ along itself. 

In the proof, he reduces the claim to the following assertion: 

 > Let $\mathcal{C}\subset \mathcal{P}(S)$ be the essential image of the Yoneda embedding. Let $X\in\mathcal{P}(S)$ be an arbitrary object and $s$ an arbitrary object. Set $\mathcal{E}=(\mathcal{C}_{/X})^\triangleright\times_{\mathcal{P}(S)}(\mathcal{P}(S)_{j(s)/})$ and $\mathcal{E}^0=(\mathcal{C}_{/X})\times _{(\mathcal{C}_{/X})^\triangleright}\mathcal{E}$. Then the inclusion $\mathcal{E}^0\subset \mathcal{E}$ is a weak homotopy equivalence. 


Lurie then finishes the proof by claiming that both $\mathcal{E}$ and $\mathcal{E}^0$ deformation retracts onto $\mathcal{E}^1= \mathcal{C}_{/X}\times _{\mathcal{C}}\{\operatorname{id}_{\mathcal{C}}\}$. **It is this very last step I am having trouble understanding.** Why do $\mathcal{E}$ and $\mathcal{E}^0$ deformation retract onto $\mathcal{E}^1$?  It is easy to see that they both have the homotopy type of $\operatorname{Map}_{\mathcal{P}(S)}(j(s),X),$ so I know that the claim isn't unreasonable. Also, the claim is easy to see if we are working with ordinary categories (and set-valued presheaves); but the proof (or my proof) does not seem to carry on direclty to the $\infty$-categorical case, because it relies heavily on the strict composition of 1-categories.

Any help (including alternative ways to see that $\mathcal{E}^0\subset \mathcal{E}$ is a weak homotopy equivalence, or even alternative proofs of Lemma 5.1.5.3) is appreciated. Thanks in advance.


  [1]: https://math.stackexchange.com/questions/3974923/proof-of-lemma-5-1-5-3-in-jacob-luries-htt