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.