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

  • (no subject)

    I doubt any of the 5+/-2 people still reading this need to be encouraged to vote. One more day. Fingers crossed.

  • (no subject)

    I guess I have watched all three debates for whatever reason. I have as an axiom in the back of my head to generally distrust statements of the form…

  • (no subject)

    Uh-oh, elder gods invading the midwest, y'all.

  • 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