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)

    After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

  • (no subject)

    Went to a series of maker-y talks hosted by Pivotal. The last one, by the woman who runs Genspace, "New York City's Community Biolab" was pretty…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • 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