So of course I tried to prove it in homotopy type theory:
See
https://github.com/jcreedcmu/HoTT-Agda/blob/master/Spaces/SInfinity.agda
for a definition of S∞ and
https://github.com/jcreedcmu/HoTT-Agda/blob/master/Spaces/SInfinityIsContr.agda
for a proof that the map that self-embeds it in its own equator is homotopy-equivalent to the identity, which has as a corollary that it's contractible, because every point in the equator uniformly has a path to the north pole, and such an equivalence means every point uniformly has a path to the north pole.
But, sadly, my proof is wrong, and (unknown to me while I was proving it --- I only found out after tinkering with some other things) exploits a bug in agda's --without-K flag. Gonna try to fix it.
