Jason (jcreed) wrote,
Jason
jcreed

A while ago I came across this neat list of surprising results in math and one I hadn't heard of is that the infinite-dimensional sphere is contractible, unlike all the finite-dimensional spheres.

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.
Tags: hott, math
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 3 comments