Resurrect ancient `Pi1S1.v`?

[peterlefanulumsdaine]

contrib/old/Pi1S1.v had been pseudo-deleted (i.e. removed from the Makefile) at some point in the past, and was fully deleted in #1338. Its material is still conceivably of interest — an elementary, self-contained, and quite human-readable calculation of Pi_1(S^1), which (on a cursory search) is no longer present in the library (i.e. the result is still present, but not in such a nicely readable form) — but it is extremely stale, so may be quite difficult to bring up to date.

• Do we think it would be nice to resurrect this file?
• Is anyone willing to do the work?

In principle I would support restoring this, if anyone feels like doing so (probably in contrib since it’s a “bonus extra” wanted just for intrinsic interest). However, I’m probably not going to do so myself any time soon — it feels fairly low priority.

[Alizter]

I'm happy to resurrect this at some point. This is the "homotopy theoretic proof" of Pi1S1 that is presented in the book. We only have the encode-decode one. Whether people should actually use this proof over the encode-decode one I am unsure. I think it is probably better to keep the encode-decode one as the main proof and put this proof in a module inside Homotopy/Pi1S1.v where it can be seen and imported if need be, but but not imported by default when you import Homotopy.Pi1S1.

[mikeshulman]

I feel similarly -- it would be nice to keep somewhere that's not imported by default, but I'm not available to do the work of making it compile.

[Alizter]

I should be a bit more clear. I think it should be in a module inside HIT/Circle.v rather than Pi1S1.v as this is just a calculation that the loop space of the circle is equivalent to the integers.

[peterlefanulumsdaine]

Thankyou @Alizter — resurrecting this would be great, and I agree, a module inside HIT/Circle.v sounds good.

[Alizter]

I've been working on this and it seems to me that this file is quite stale. A lot of effort is spend manually computing on point constructors (since the private inductive type trick was unknown). I've begin rewriting it from scratch, adding comments comparing it to the encode-decode proof. The proofs are very similar apart from how an equivalence is constructed. In the encode-decode proof the equivalence is explicitly shown to exist, whereas in the "homotopy theoretic" proof, the total space of the universal cover of the circle (the homotopyical reals) is shown to be contractible. Since the total space of a path fibration is also contractible, we get an induced fiberwise equivalence. All the work in this proof is showing that the "homotopical reals" are contractible.