Path loop fibration and its connecting isomorphisms

Apply F1 to the based map from one point to $X$. Its mapping-path total space identifies with $PX$ and its fiber over $x_0$ with $\mathrm{\Omega }X$ by F2. The contraction is $D(\alpha ,t)(s)=\alpha ((1-t)s)$, with $D(-,0)=\mathrm{i}\mathrm{d}$ and $D(-,1)=c_{x_0}$; it fixes the constant path and is jointly continuous by the F1 proof. Thus every based cube in $PX$ contracts rel boundary by this formula, so its positive homotopy groups vanish and its component set is a singleton.

For a cube $b(u,t)$ representing a class in $X$, a terminal-point lift is $\tilde{b}(u,t)(s)=b(u,1-(1-t)s)$. It starts at $x_0$ as a path in $s$, ends at $b(u,t)$, is constant when $t=1$ or $u$ is on its boundary, and is continuous by the same interval evaluation/transposition as F1. Its distinguished face is $u\mapsto (s\mapsto b(u,1-s))$. For $n=1$ this is precisely the reverse loop. This directly verifies the orientation rather than assuming a sign-free identification.

For $n\ge 2$, the exact segment ${\pi }_n(PX)\to {\pi }_n(X)\stackrel{\mathrm{\partial }}{\to }{\pi }_{n-1}(\mathrm{\Omega }X)\to {\pi }_{n-1}(PX)$ has zero outer groups by step 1.1. Hence $\mathrm{\partial }$ is both injective and onto. In degree one, exactness shows onto ${\pi }_0(\mathrm{\Omega }X)$, since $PX$ has one component. More explicitly the F3 action is transitive, and its stabilizer is the image of the zero group ${\pi }_1(PX)$; therefore its orbit map, and its composite with loop inversion, are bijections.

A based space is nonempty. If $X$ is one point all groups and component sets in the assertion are trivial; additional components of a general $X$ need not be reached by $PX\to X$ and do not affect its based sequence. The computations explicitly include the constant loop, both time endpoints, and degree one without inventing a group law on a general component set. All lifts and contractions used here are specified formulas, hence choice-free.