Topological four-dimensional Poincaré theorem

Let $S^4=\{x\in\mathbb R^5:\|x\|=1\}$ with the Euclidean subspace topology. For every type $M$ in the base universe equipped with a topology making it compact and Hausdorff and with a specified charted-space structure modeled on $\mathbb R^4$, existence of a continuous homotopy equivalence between $M$ and $S^4$—that is, a pair of continuous maps in opposite directions whose two composites are continuously homotopic to the corresponding identity maps—implies existence of a homeomorphism $M\to S^4$. There is no differentiability or smooth-compatibility assumption on the chart structure and no smoothness conclusion. The homeomorphism is required only to exist, without uniqueness or a prescribed homotopy class. Empty $M$ is allowed by the quantified space assumptions, but its homotopy-equivalence premise cannot hold.