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 contractible total space has CW homotopy type and the base is a CW complex. Apply [F4] to the Hurewicz fibration of step 1.2: its strict loop fiber has CW homotopy type. 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 used only to select the CW-type representative and through marked uniqueness in step 2.1; the mapping-path formulas and exact-sequence calculations add none. There is no converse assertion.