A simply connected CW homology equivalence is a homotopy equivalence under the stated choice conditions

Apply [F1] to the empty fixed subcomplex to obtain a cellular map $g:X\to Y$ and a homotopy $E:f\simeq g$. Use its finite clause when $X,Y$ are finite; otherwise use [A1]. By the prism identity [F3], $g_{\ast }=f_{\ast }$ in each homology degree, so $g$ is also a homology equivalence. Form its ordinary CW cylinder $M$ with source $j:X\hookrightarrow M$, target $k:Y\hookrightarrow M$ and retraction $r:M\to Y$ in [F2]. Then $rj=g$, $rk=\mathrm{i}\mathrm{d}$ and $kr\simeq {\mathrm{i}\mathrm{d}}_M$. Thus $r_{\ast }$ in homology has inverse $k_{\ast }$ by [F3], and $j_{\ast }=r_{\ast }^{-1}{g}_{\ast }$ is an isomorphism in every degree.

For $i\ge 1$ consider $H_i(X)\stackrel{j_{\ast }}{\to }{H}_i(M)\to H_i(M,j(X))\stackrel{\delta }{\to }{H}_{i-1}(X)\stackrel{j_{\ast }}{\to }{H}_{i-1}(M)$. Since the rightmost map is injective, every relative class has zero boundary and comes from $H_i(M)$. Since the leftmost map is surjective, that entire image in the relative group is zero. Hence $H_i(M,j(X))=0$. In degree zero the relative group is the cokernel of the surjective $j_{\ast }:H_0(X)\to H_0(M)$, so it too is zero.

The space $M$ is path connected: each of its points has its cylinder track to $k(Y)$, and $Y$ is path connected. The retraction's all-basepoint homotopy isomorphisms [F2] show ${\pi }_1(M,j(x))=0$ for every $x\in X$, since $Y$ is simply connected. Both component sets of $j(X)$ and $M$ are singletons. The pointed tail in [F4] therefore shows that every relative degree-one class comes from ${\pi }_1(M,j(x))$ and is distinguished. Thus the CW pair $(M,j(X))$ is $1$-connected in the exact sense of [F4], and its subspace is nonempty and simply connected.

Induct on the integer $n\ge 2$. Suppose the pair is $(n-1)$-connected, starting with step 2.2. At each arbitrary $x\in X$, [F5] identifies ${\pi }_n(M,j(X),j(x))$ with $H_n(M,j(X))=0$ from step 2.1. Hence all these relative groups vanish, and the component condition is unchanged, so [F4] makes the pair $n$-connected. Induction proves vanishing in every positive relative degree at every $x$. This is induction on a property, not the selection of an infinite sequence of homotopies or inverse maps. In particular its use of [F5] is choice-free even though its all-data weak model can be infinite.

For every $i\ge 1$ the exact segment ${\pi }_{i+1}(M,j(X),j(x))\to {\pi }_i(X,x)\stackrel{j_{\ast }}{\to }{\pi }_i(M,j(x))\to {\pi }_i(M,j(X),j(x))$ has trivial outside terms by step 3.1. Exactness gives zero kernel and full image for the middle homomorphism. This also works for $i=1$, whose right outside object is pointed rather than a group. The component bijection was checked in step 2.2. Thus $j$ is weak by [F6]. The retraction in [F2] is weak at all basepoints, so $g=rj$ is weak, including its component map.

Apply Whitehead [F6] to $g:X\to Y$. Under [A1] its general clause applies. For finite $X,Y$, its finite clause applies and requires no choice; the preceding approximation used its finite clause and the Hurewicz comparison was choice-free. Let $h:Y\to X$ be the resulting homotopy inverse, so $hg\simeq {\mathrm{i}\mathrm{d}}_X$ and $gh\simeq {\mathrm{i}\mathrm{d}}_Y$. Composing $E$ with $h$ on its two sides gives $hf\simeq hg$ and $fh\simeq gh$. Concatenation gives both $hf\simeq {\mathrm{i}\mathrm{d}}_X$ and $fh\simeq {\mathrm{i}\mathrm{d}}_Y$, proving the conclusion for the original $f$. These are unbased homotopies, so the approximation never required an unstated fixed basepoint.

Empty endpoint complexes are excluded by the stated meaning of simply connected; a point endpoint or an identity map satisfies the same argument. All relative homology groups, including degree zero, were checked in step 2.1, and the first induction degree $n=2$ meets [F5]'s simple-connectivity hypothesis by step 2.2. No finite-dimensional upper bound is needed for the induction on group vanishing. The finite branch has only finite approximation and finite Whitehead choices; the arbitrary branch uses [A1] exactly in [F1] and [F6]. Both homotopy-inverse identities are established in step 5.1, with no conclusion asserted for non-simply-connected spaces.