The first Hurewicz map is abelianization

A constant edge is the boundary of the constant singular two-simplex, since its three boundary terms have coefficients $1,-1,1$. If $a,b$ are composable paths, define $s:{\mathrm{\Delta }}^2\to X$ as $(a\ast b)\circ \mathrm{\ell }$, where in barycentric coordinates $\mathrm{\ell }(t_0,t_1,t_2)=t_1\mathrm{/}2+t_2$. On edges $01,12,02$ it gives respectively $a,b,a\ast b$, so $\mathrm{\partial }s=b-(a\ast b)+a$ and $a\ast b\sim a+b$. If two paths are homotopic with endpoints fixed, [F4] says their difference is a prism boundary plus a difference of constant endpoint edges, which are themselves boundaries as just proved; hence they are equivalent under $\sim$. Finally $a\ast \bar{a}$ contracts rel endpoints by retracing shorter initial segments: on the two half-intervals use $a(2t(1-s))$ and $a(2(1-t)(1-s))$. Therefore $\bar{a}\sim -a$. All these are finite chain relations.

For a finite singular cycle $c={\sum }_e{m}_{e}e$, let $V$ be its finite set of endpoints together with $x_0$. By path-connectedness and [F6], there are paths $p_v:x_0\to v$ for $v\in V$, with $p_{x_0}$ the constant path. Define $T_p(c)={\sum }_e{m}_e[p_{e(0)}\ast e\ast {\bar{p}}_{e(1)}{]}_{\mathrm{a}\mathrm{b}}\mathrm{.}$ Repeated edges may be combined and zero coefficients removed; the sum is finite and lies in $G^{\mathrm{a}\mathrm{b}}$.

The map in [F1] sends a loop, viewed as a singular one-cycle, to its homology class. To verify the generator identification, realize the oriented circle as the boundary of a positively oriented triangle. Its boundary is $e_{01}+e_{12}-e_{02}$ by [F3]. In that triangle-boundary simplicial complex, the one-cycle condition forces the three oriented edge coefficients to be equal, and there are no two-simplices, so this alternating boundary is a primitive positive generator; [F7] transfers that generator to singular homology. Step 1.1 identifies this class with the single positively traversed loop $e_{01}\ast e_{12}\ast {\bar{e}}_{02}$. Its parametrization gives the positive based identification $I\mathrm{/}\mathrm{\partial }I\cong S^1$, so postcomposing it with any based sphere map gives exactly the singular loop representing that based class, up to endpoint-fixed reparametrization. Thus $h([a])=[a]$ in singular homology with the stated orientation. Since $h$ is a homomorphism into an abelian group, [F5] factors it uniquely as $\bar{h}:G^{\mathrm{a}\mathrm{b}}\to H_1(X)$.

This value is independent of the chosen finite paths. For another family $p_v^{\mathrm{\prime }}$, put $d_v=[p_v^{\mathrm{\prime }}\ast {\bar{p}}_v{]}_{\mathrm{a}\mathrm{b}}$. Canceling a path followed by its reverse, with the retracing homotopy of step 1.1, gives $[p_{e(0)}^{\mathrm{\prime }}\ast e\ast {\bar{p}}_{e(1)}^{\mathrm{\prime }}{]}_{\mathrm{a}\mathrm{b}}=d_{e(0)}+[p_{e(0)}\ast e\ast {\bar{p}}_{e(1)}{]}_{\mathrm{a}\mathrm{b}}-d_{e(1)}\mathrm{.}$ The difference of the two sums is therefore ${\sum }_e{m}_e(d_{e(0)}-d_{e(1)})$. For each vertex its coefficient is the negative of its coefficient in $\mathrm{\partial }c$, hence zero. Enlarging $V$ does not change the sum either. Thus there is one uniquely defined value $T(c)$ for each cycle, without choosing paths for all points of $X$. For two cycles choose paths on the union of their finite vertex sets; the same formula then proves $T(c+c^{\mathrm{\prime }})=T(c)+T(c^{\mathrm{\prime }})$ and $T(0)=0$.

This homomorphism on cycles kills boundaries. For one singular triangle $\sigma$, choose paths to its three vertex images and $x_0$. Write $a_{ij}=\sigma {\mathrm{\mid }}_{[i,j]}$ and $L_{ij}=p_{\sigma (i)}\ast a_{ij}\ast {\bar{p}}_{\sigma (j)}$. The path $a_{01}\ast a_{12}$ is endpoint-fixed homotopic to $a_{02}$: in the convex triangle, interpolate the broken two-edge parametrized path linearly to the direct $02$ edge, then compose with $\sigma$. Cancellation of the middle $p$ and reversed $p$ shows $[L_{01}][L_{12}]=[L_{02}]$ in $G$. Thus the value assigned to $\mathrm{\partial }\sigma$ is $[L_{12}{]}_{\mathrm{a}\mathrm{b}}-[L_{02}{]}_{\mathrm{a}\mathrm{b}}+[L_{01}{]}_{\mathrm{a}\mathrm{b}}=0$. For an arbitrary finite two-chain, choose paths on the finite union of all its vertex images and apply this calculation term by term, with its integer coefficients. Any cancellation among its boundary edges also cancels the corresponding loop terms. By the independence in step 2.2 this proves $T(\mathrm{\partial }b)=0$ for every two-chain $b$. Therefore $T$ descends to a homomorphism $\tilde{T}:H_1(X)\to G^{\mathrm{a}\mathrm{b}}$.

For a cycle $c={\sum }_e{m}_{e}e$, step 1.1 gives $p_{e(0)}\ast e\ast {\bar{p}}_{e(1)}\sim p_{e(0)}+e-p_{e(1)}\mathrm{.}$ Summing with coefficients $m_e$, the $p_v$ terms cancel exactly because $\mathrm{\partial }c=0$. The sum of the based loops is therefore homologous to $c$. By step 2.1 this says $\bar{h}\tilde{T}([c])=[c]$. Conversely, for a based loop $a$ choose only the constant path to its sole endpoint $x_0$. Its defining sum gives $T(a)=[a{]}_{\mathrm{a}\mathrm{b}}$, so $\tilde{T}\bar{h}([a{]}_{\mathrm{a}\mathrm{b}})=[a{]}_{\mathrm{a}\mathrm{b}}$. Every element of $G^{\mathrm{a}\mathrm{b}}$ is the coset of some element represented by a based loop, hence these are inverse maps on the whole groups.

Thus $\bar{h}$ is an isomorphism. Since $h=\bar{h}\circ (G\to G^{\mathrm{a}\mathrm{b}})$, it is onto and its kernel is exactly the kernel of the quotient, namely the commutator subgroup. Naturality follows from [F1] and [F5]: a based map commutes with $h$ and induces the map of universal abelian quotients, so it commutes with $\bar{h}$, and then also with its inverse. No global family of transport paths is used in this conclusion.

The zero cycle uses just the basepoint path and gives zero; integer coefficients, negative coefficients, repeated simplices and degenerate triangles were handled by linearity and the explicit triangle relations. For a singleton target, all loops are constant and all one-cycles are boundaries, so both groups are zero. Empty $X$ has no basepoint and is not an instance. The proof uses path-connectedness exactly to supply paths for the finite vertex sets in steps 1.2 and 3.1. Finite choice suffices for each such set, and independence specifies a unique value for every cycle; no AC or countable choice is used. Endpoint-fixed path homotopies and first-loop-first order were retained throughout.