Density Theorem for $\infty$-Categories (HTT, Lemma 5.1.5.3) 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), 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}_{j(s)}\}$. 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.
 A: I'm going to deal with the case of  $\mathcal E^1\subset \mathcal E^0$. Note that by composition of pullbacks, $\mathcal E^0 = \mathcal C_{/X}\times_{\mathcal P(S)}\mathcal P(S)_{j(s)/}$, while $\mathcal E^1= \mathcal C_{/X}\times_\mathcal C\{j(s)\}$.
Further, because $\mathcal C\to \mathcal P(S)$ is a full subcategory inclusion, you can rewrite $\mathcal E^0 = \mathcal C_{/X}\times_\mathcal C \mathcal C_{j(s)/}$
Now we write the obvious thing : the homotopy $\mathcal E^0\times\Delta^1\to \mathcal E^0$ should be given by the following thing:

*

*on the $\mathcal C_{j(s)/}$ factor, go $\mathcal E^0\times\Delta^1\to \mathcal C_{j(s)/}\times\Delta^1\to \mathcal C_{j(s)/}$ where the second map is the canonical homotopy witnessing that $\mathcal C_{j(s)/}$ deformation retracts onto $\{j(s)\}$;

*on the $\mathcal C$ factor, same as above but postcompose further with $\mathcal C_{j(s)/}\to \mathcal C$

*On the $\mathcal C_{/X}$ factor, you'll have to observe that there is a composition map $\mathcal C_{/X}\times_\mathcal C \mathcal C_{j(s)/}\to map(X,j(s))$. Indeed this is like $\{j(s)\}\times_{\hom(\{0\},\mathcal C)} \hom(\Lambda^2_1,\mathcal C)\times_{\hom(\{2\}, \mathcal C)} \{X\}$, and the forgetful map $\hom(\Delta^2,\mathcal C)\to \hom(\Lambda^2_1,\mathcal C)$ is an acyclic fibration, so in particular has a section. So you can use that section, and then evaluate on $\Delta^{\{0,2\}}$, and forget about the $\{j(s)\}\times_{\hom(\{0\},\mathcal C)}$ part to land in $\hom(\Delta^1,\mathcal C)\times_{\hom(\{2\},\mathcal C)}\{X\}= \mathcal C_{/X}$.

Here I'm being a bit sloppy between $\mathcal C_{/X}$ and $\hom(\Delta^1,\mathcal C)\times_{\hom(\{1\},\mathcal C)}\{X\}$ (I always forget whether they are literally isomorphic or just equivalent) but they are equivalent so it does not really matter.
So now, you have an equivalence ${}_{j(s)}\hom(\Lambda^2_1,\mathcal C)_X\to {}_{j(s)}\hom(\Delta^2,\mathcal C)_X$, and the point is now that there is a homotopy $\Delta^1\times\hom(\Delta^2,\mathcal C)\to \hom(\Delta^1,\mathcal C)$ that more or less witnesses the fact that there is a map from $0\to 2$ to $1\to 2$ in the triangle $\Delta^2$, and so if you string these together, you will get a homotopy $\Delta^1\times\mathcal E^0\to \mathcal C_{/X}$ that looks exactly like the natural transformation $(j(s)\to y\to  X, j(s) = j(s))\to (y\to X, j(s)\to y)$ that you would write down $1$-categorically.
Now these three homotopies are compatible and so they do assemble as a map from $\mathcal E^0\times\Delta^1$ to the pullback,  which is precisely $\mathcal E^0$. It is clear from the construction that it starts at the identity, and ends in $\mathcal E^1$.
Basically the key point here was the third homotopy: given what you wrote in your question about "composition", I'm guessing that this is what was missing. In particular, I would suggest trying to see if you can do the same kind of the thing for the case of $\mathcal E$, and replace the words "compose" in your $1$-categorical proof with something along the lines of what I did here. If that doesn't work, let me know and I'll try to modify my answer to incorporate that part as well.
Also note that, as Zhouhang pointed out in the comments, Kerodon has a different proof of this fact altogether, or rather it's arranged differently : it observes that the yoneda embedding is dense, and earlier proved that if $f : C\to D$ is dense, then the identity of $D$ was the left Kan extension of $f$ along itself (and also relates this to the condition that the "canonical diagram" be a colimit diagram). It feels like a better proof, so I would suggest looking at that too.
A: Let me post this answer so that the key point will not be buried in the comments. Maxime has wonderfully dealt with the case of $\mathcal{E}^0$. (Incidentally, this follows from the fact that $\mathcal{C}_{/X}\to\mathcal{C}$ is a right fibration, hence proper.) For $\mathcal{E}$, consider the final functor $(\mathcal{C}_{/X})^\triangleright\to\mathcal{P}(S)_{/X}$ over $\mathcal{P}(S)$ which extends the inclusion $\mathcal{C}_{/X}\hookrightarrow \mathcal{P}(S)_{/X}$ and maps the final vertex to the final object $\operatorname{id}_X$. The map $\mathcal{E}^1\to\mathcal{P}(S)_{/X} \times_{\mathcal{P}(S)}\{\operatorname{id}_{j(s)}\}$ is an isomorphism of simplicial sets, so it suffices to show that the inclusion $\mathcal{P}(S)_{/X} \times_{\mathcal{P}(S)}\{\operatorname{id}_{j(s)}\}\hookrightarrow\mathcal{P}(S)_{/X}\times_ {\mathcal{P}(S)}\mathcal{P}(S)_{j(s)/}$ is a weak homotopy equivalence.
But this, again, follows from an argument in line with Maxime's answer. The situation can be summarized in the diagram below, whose squares are all cartesian.
$$\require{AMScd}
\begin{CD}
\mathcal{E}^1 @>>> \mathcal{E}^1 @>>> \mathcal{P}(S)_{/X}\times_{\mathcal{P}(S)} \{\operatorname{id}_{j(s)}\} @>>> \{\operatorname{id}_{j(s)}\}\\
@VVV @VVV @VVV @VVV\\
\mathcal{E}^0 @>>>\mathcal{E} @>>> \mathcal{P}(S)_{/X} \times_{\mathcal{P}(S)} \mathcal{P}(S)_{j(s)/} @>>>\mathcal{P}(S)_{j(s)/}\\
@VVV @VVV @VVV @VVV\\\
\mathcal{C}_{/X}@>>> (\mathcal{C}_{/X})^\triangleright @>>>\mathcal{P}(S)_{/X} @>>>\mathcal{P}(S).
\end{CD}
$$
A: I give different arguments for this kind of things here. In short, the main case is the one of the terminal presheaf: one proves by cofinality arguments that the colimit of the Yoneda embedding $S\to\mathcal P(S)$ is isomorphic to the colimit of the identity of $\mathcal P(S)$; since $\mathcal P(S)$ has a terminal object, this colimit has to be the value of the identity at the terminal object, hence the terminal object itself. For a general presheaf $F$, one replaces $S$ by the category of elements $S/F$ and uses the fact that left Kan extending along the projection $S/F\to S$ sends the termnal object of $\mathcal P(S/F)$ to $F$ (and preserves colimits, being a left adjoint).
Here are more precise references. The main observation is that, given any functor $u:A\to B$, the map $S(A)\to (A^{op}\times B)\times_{B^{op}\times B}S(B)$ is limit-cofinal, where $S(A)=Tw(A)^{op}$ is the opposite of the twisted arrow category; this is Prop. 5.6.9 in loc. cit. In the case where $u$ is the Yoneda embedding, this leads to a proof that the left Kan extension along the Yoneda embedding is the identity of the category of presheaves on a small category (this is essentially Lemma 5.8.11 and the proof of Prop. 6.2.13). This leads to a proof of the Yoneda lemma itself (Theorem 5.8.13). This also implies rather directly that the colimit of the Yoneda embedding is the terminal object (Prop. 6.2.13), from which the property you ask for follows right away: any presheaf is a colimit of representable presheaves (Cor. 6.2.16). The fact that presheaves categories are dualizable objects among cocomplete categories is also a direct consequence of the kind of cofinality provided by Prop. 5.6.9 (Theorem 6.7.2).
