Proof of Lemma 5.1.5.3 in Jacob Lurie's HTT. I am currently trying to understand the following proof in Higher Topos Theory.



I am fine with almost all of the argument, except with the claim that $\mathcal{E}^1$ is a deformation retract of $\mathcal{E}$. While I feel like this is true, I am unable to prove it properly, i.e writing down a well-defined morphism of simplicial sets $r : \mathcal{E} \to \mathcal{E}^1$ along with a homotopy witnessing it as a deformation retract.
An object (i.e a $0$-simplex) of $\mathcal{E}^1$ is just a map $C \to X$ in $\mathcal{P}(S)$, while an object of $\mathcal{E}$ is

*

*Either a couple $(v, C \to X)$ where $v$ is the cone point of $(\mathcal{C}_{/X})^\rhd$.

*Either a couple $(B \to X, C \to B)$ where $B$ is in $\mathcal{C}$.

The "obvious way" to produce a map $C \to X$ out of this kind of data would be to send $(v, C \to X)$ to $C \to X$ and $(B \to X, C \to B)$ to a composition $C \to B \to X$. My issue with this approach is that I am using composition internal to $\mathcal{P}(S)$, which is only weakly defined, and I do not know how to produce a full map of simplicial sets using it. The same problem arises when trying to work out higher-dimensional simplices.
I can show that $\mathcal{E}^1 \to \mathcal{E}^0$ is a weak homotopy equivalence by viewing it as a pullback of the initial (hence left anodyne) map $\{\mathrm{id}_{\mathcal{P}(S)}\} \hookrightarrow \mathcal{P}(S)_{C/ }$ by the right fibration (hence proper map) $\mathcal{C}_{/X} \to \mathcal{C}$. I can not make this argument work for $\mathcal{E}^1 \to \mathcal{E}$, unless the map $(\mathcal{C}_{/X})^\rhd \to \mathcal{P}(S)$ is proprer. I have no idea wether this can be expected or not.
Using a similar kind of argument (pulling back the right anodyne map $\{v\} \to (\mathcal{C}_{/X})^\rhd$ along the left fibration $\mathcal{P}(S)_{C/ } \to \mathcal{P}(S)$), I can show that $\mathcal{E}^0$ indeed has the same homotopy type as $\mathcal{E}$ and that it is the homotopy type of $\mathrm{Map}_{\mathcal{P}(S)}(C, X)$ but this argument does not say that this equivalence is induced by $\mathcal{E}^0 \to \mathcal{E}$.
Is there a simple argument to show that $\mathcal{E}^1 \to \mathcal{E}$ is a weak homotopy equivalence, or even to show directly that $\mathcal{E}^0 \to \mathcal{E}$ is a weak homotopy equivalence?

Update: It seems to me that one can show directly that $\mathcal{E}^0$ is a deformation retract of $\mathcal{E}$, and that the homotopies do not use composition internal to $\mathcal{P}(S)$. However, I am not yet been able to write the homotopy either, and would appreciate any hint or construction that would help defining such a map.
 A: I think you are right in following intuitions at the zero level, but I strongly recommend you not to use simplex by simplex constructions and use abstract stuff to create maps, as you were doing.
My first intuition was the following (see HTT 1.2.2 for definitions):

*

*$\mathcal{E}$ can be contracted to the cone point in the first component, yielding $\text{Hom}^L_{\mathcal{P}(S)}(C,X)$;

*$\mathcal{E}_0$ can be contracted in the second component (because the overcategory has a final object) to yield exactly $\mathcal{E}^1 = \text{Hom}^R_{\mathcal{P}(S)}(C,X)$;

The very non obvious thing is then to find a deformation retraction from $\text{Hom}^L \to \text{Hom}^R$, which I am not quite sure it exist; so we should change approach. On the other side, we can contract the second component on $\{1_C\}$ because it is initial, yielding a deformation retraction
$$ \mathcal{E} \to (\mathcal{C}_{/X})^{\triangleright} \times_{\mathcal{P}(S)} \{1_C\} $$
But the cone point is sent to $X \in \mathcal{P}(S)$ and will never contribute to the pullback, so the latter is equal to $\mathcal{E}^1$! This happens unless $X=C$, but in this case the inclusion $\mathcal{C}_{/C} \to (\mathcal{C}_{/C})^{\triangleright}$ is a deformation retraction by sending the cone point to $1_C$.
I don't know which lemma to invoke here so we just verify on simplices: an $n$ simplex $\Delta^n \to (\mathcal{C}_{/X})^{\triangleright} \times_{\mathcal{P}(S)} \{1_C\}$ is the same as a map $\phi : \Delta^{k+1} \to \mathcal{C}$ for some $-1 \le k \le n$  so that
$$\phi(k+1) = X, \ \ \  \phi|_{\{0, \ldots, k\}} * X : \Delta^n \to \mathcal{C} $$
is constantly $C$, where $X$ above denotes the constant $=X$ simplex $\Delta^{n-k-1} \to \mathcal{P}(S)$. In order for this to happen, we must have $n-k-1 = -1$ because $X \neq C$, i.e. $n=k$. But $n$ simplices $\phi: \Delta^{n+1} \to \mathcal{C}$ such that
$$\phi(n+1) = X, \ \ \ \phi|_{\{0, \ldots, n\}} = C $$
are exactly the simplices coming from $\mathcal{C}_{/X} \times_{\mathcal{P}(S)} \{1_C\}$.
Remark. I implicitly used above that maps $\Delta^n \to A^{\triangleright}$ are the same as maps $\phi:\Delta^k \to A$ with $-1 \le k \le n$, and under a simplicial map $F: A^{\triangleright} \to B$ such simplex is sent to $ F( \phi)* F(v)* \ldots * F(v)$; here $v$ is the cone point and $F(v)$ is repeated $n-k-1$ times. This is just another way of stating that
$$ (A^{\triangleright})_n = (A * \Delta^0 ) = A_n \cup (\Delta^0)_n \cup \bigcup_{i+j = n-1} A_i \times (\Delta^0)_j $$
Using the convenient convention that $\Delta^{-1} = \emptyset$, so that $A_{-1}$ has just one element (the empty map).
A: I asked this question again in MO and Maxime Ramzi gave a perfect answer. See here.
