Proof Sketch: The pullback of the inclusion of the 0th vertex into the standard n-simplex by a right fibration is a deformation retract (450 point bounty if answered by 2am EST)

Question

I was not sufficiently clear on my last attempt at asking a similar (but not identical) question. Tom Goodwillie mentioned (in the accepted answer) that the question can be reduced to this one and mentioned a fact of which I was unaware, but after trying to prove this for the past day, I have returned to ask for a sketch of the proof:

Let $X$ be a simplicial set, and let $p:X\to \Delta^n$ be a right fibration (has the right lifting property with respect to all right horn inclusions (equivalently, it has the right lifting property with respect to the maps $$\Delta^1\times A\coprod_{\{1\}\times A}\{1\}\times B\to \Delta^1\times B$$ for any inclusion $A\hookrightarrow B$). (These generate the same weakly saturated class of maps)).

Let $i_0:\{0\}\hookrightarrow \Delta^n$ be the inclusion of the 0th vertex of $\Delta^n$. We'd like to show that the pullback of this map by $p$ (i.e. the induced map $f:X\times_{\Delta^n} \{0\}\hookrightarrow X$) is a deformation retract.

According to Tom, we can use the second characterization of right fibrations to obtain some kind of lifting of the homotopy and retraction for $i_0$ (which is a deformation retract).

Would somebody mind sketching the proof?

Edit: If this question is answered by 2AM EST (roughly three hours and forty-five minutes from the time of this current edit), I will award the answerer with a 450 point bounty as soon as it becomes possible (one must wait 48 hours from when the question was asked).

Answer 1

Harry, let $Y$ be the fiber of $X\to\Delta^n$ over the 0th vertex. The sense in which $Y$ is going to be a deformation retract of $X$ is going to be the following: There is a map $\Delta^1\times X\to X$ such that (1) on $1\times X$ it's the identity and (2) on $\Delta^1\times Y$ it's the constant homotopy (i.e. projection to $Y$ followed by inclusion) and (3) it takes $0\times X$ to $Y$. This is the same sense in which the 0th vertex is a deformation retract of $\Delta^n$.

So make a square in which the upper left object is $\Delta^1\times Y\cup 1\times X$, the lower left is $\Delta^1\times X$, the left map is inclusion, the right-hand map is the given right fibration $p:X\to \Delta^n$, the upper map is inclusion into $\Delta^1\times X$ followed by projection of $\Delta^1\times X$ to $X$, and the lower map is $Id\times p$ to $\Delta^1\times \Delta^n$ followed by the deformation retraction to $\Delta^n$.

A slanting arrow $\Delta^1\times X\to X$ making the triangles commute will have the desired restriction to $\Delta^1\times Y\cup 1\times X$ because of the upper triangle, and will take $0\times X$ into $Y$ because of the lower triangle.