Circle and path-loop models for Eilenberg–Mac Lane induction

The quotient circle is connected by the paths $t\mapsto [tx]$ and has its standard one-vertex, one-edge CW structure. Its marked fundamental group is $\mathbb{Z}$ by [F1]. The cover in [F1] is a Hurewicz fibration with discrete fiber $\mathbb{Z}$. Every positive-dimensional cube in that fiber is constant, while contractibility makes every positive homotopy group of $\mathbb{R}$ zero. The long exact sequence [F2] therefore gives ${\pi }_i(S^1)=0$ for $i>1$. This is exactly the marked $K(\mathbb{Z},1)$ condition.

Apply [F2] to the inclusion of the marked basepoint $\ast \to K(A,n)$. Its mapping-path total space is the based path space $PK(A,n)$, its endpoint map is Hurewicz, its strict fiber is $\mathrm{\Omega }K(A,n)$, and the explicit path-shrinking deformation contracts the total space to the constant path. Exactness gives ${\pi }_i(\mathrm{\Omega }K(A,n))\cong {\pi }_{i+1}(K(A,n))(i\ge 1)\mathrm{.}$ The component segment and ${\pi }_1(K(A,n))=0$ show that the loop fiber is path connected. Thus its only nonzero positive homotopy group is $A$ in degree $n-1$, marked by the displayed connecting isomorphism.

The marked base $K(A,n)$ is a nonempty connected CW complex. Apply [F4] directly to this base and its marked point: the actual based loop space, which is the strict fiber in step 1.2, has CW homotopy type in the topology used by [F2]. Choose a CW complex $L$ and a homotopy equivalence $L\to \mathrm{\Omega }K(A,n)$, transporting the connecting marking to $L$. Step 1.2 makes $L$ a marked $K(A,n-1)$, including the degree-one case $n=2$. Marked uniqueness [F3] supplies a homotopy equivalence from the chosen $K(A,n-1)$ to $L$ inducing the prescribed identification; composing gives the asserted marked equivalence with the strict loop fiber.

All spaces are nonempty because marked basepoints are supplied. For $A=0$, step 1.2 gives a weakly contractible connected loop fiber and step 2.1 compares it with the chosen contractible CW $K(0,n-1)$. The cases $n=2$, one loop component, the zero homotopy groups, the constant path, and both ends of the long exact sequence were included. The circle calculation uses no choice. AC is inherited by the locally proved CW-type theorem [F4], is used to select its CW-type representative, and is used through marked uniqueness in step 2.1; the mapping-path formulas and exact-sequence calculations add none. There is no converse assertion.