Let $\mathcal{M}$ be the simplicial set defined by the formula $Hom( \Delta^{J}, \mathcal{M} ) =Hom( \Delta^{J^{op} } \star \Delta^{J}, \mathcal{C} )$, so that an $n$-simplex of $\mathcal{M}$ is a $(2n+1)$-simplex of
$\mathcal{C}$. The inclusions of $\Delta^{J^{op} }$ and $\Delta^{J}$ into $\Delta^{J^{op} } \star \Delta^{J}$ induce a left fibration $\mathcal{M} \rightarrow \mathcal{C}^{op} \times \mathcal{C}$, which is the left fibration you are looking for. For details see section 4.2 of my paper "Derived Algebraic Geometry X", entitled "Twisted Arrow $\infty$-Categories".
Your more general question can be phrased as follows: given a coCartesian fibration
$q: X \rightarrow S$ classified by a functor from $S$ into $\infty$-categories, how can you explicitly construct a Cartesian fibration classified by the same functor? First, construct a simplicial set $Y$ with a map $Y \rightarrow S$, such that maps $T \rightarrow Y$ classify maps $T \rightarrow S$ together with maps from $X \times_{S} T$ to the $\infty$-category of spaces. Then $Y \rightarrow S$ is a coCartesian fibration, whose fibers over a vertex $s \in S$ is the $\infty$-category of presheaves on $X_{s}^{op}$. Restricting to representable presheaves determines a full simplicial subset of $Y_0 \subseteq Y$, and the map
$Y_0^{op} \rightarrow S^{op}$ is the Cartesian fibration you're looking for.
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.
![\xymatrix{ \calC^{0} \ar@{^{(}->}[d] \ar[r]^{F_0} & \calD \ar[d]^{p} \
\calC \ar[r] \ar[ur]^{F} & \calD' }](https://i.stack.imgur.com/fz1EJ.png)
Best Answer
Let me answer first the question about the homotopy pushout. It is in general not the case. Consider for instance the inclusion $\Delta^0 \to \Delta^1$. Then $\Delta^0 \star * = \Delta^1$ so that the homotopy pushout with $\Delta^1$ along $\Delta^0$ (computed as sinply the pushout, because it's along a cofibration) is just $\Lambda^2_0$, which is already a quasicategory, whereas $\Delta^1\star * = \Delta^2$, and they are not equivalent.
For the question about this comment, note that you can reformulate the statement of the lemma as : the following square is a pullback square :
$\require{AMScd} \begin{CD}D_{F/} @>>> D_{F_0/} \\ @VVV @VVV \\ D'_{pF/} @>>> D'_{pF_0/} \end{CD}$
Now in this kind of situation, a diagram in the top left hand corner which is $p$-initial when moved to the right was $p$-initial to begin with. This is 4.3.1.5.(4) in HTT.
This shows that a cocone under $F$ wich restricts to a $p$-colimit of $F_0$ is a $p$-colimit of $F$. See Daniel's comment below to see why there shouldn't be a converse in general.
Given a $p$-colimit of $F_0$, say $\overline{F_0}: C_0^\triangleright \to D$, by relative Kan extension, if you're also given an extension $\overline F : C^\triangleright \to D'$ of $p\circ \overline{F_0}$, then you get a diagram $\Delta^0\to D_{F/}$ which becomes a $p$-colimit of $F_0$ under restriction, so again by the above, a $p$-colimit of $F$.