Closed aljungstrom closed 2 months ago
@rwbarton @owen-fool maybe this is of interest to your formalisation project?
Nice! I saw your HoTT/UF abstract a couple weeks ago. I find it a bit surprising that it's possible to do cellular homology synthetically like this without having a homotopy-invariant homology theory first; I'll have to look into exactly how it works.
Of course, my burning question is: any prospects for proving the Hurewicz theorem for simply-connected finite CW complexes, in terms of this cellular homology?
@rwbarton We're hoping it should be easier but no promises yet. On the blackboard it felt like it should follow pretty easily given the appropriate theory about n-connected complexes. I'll get back to you if I make any progress.
Here's a big one... This is a bunch of code primarily written by @loic-p and me about CW complexes and cellular homology. It's part of a bigger project with @mortberg and was previously in a private repo. I guess Anders should be reviewing this one. It contains:
Cubical.CW
.Hˢᵏᵉˡ
which defines the homology of an explicitly given skeleton and then lift this toHᶜʷ
, the homology of an arbitrary CW complex, i.e. a type which is merely equivalent to the colimit of some skeleton. We have been careful to set things up so that it works for possibly infinite dimensional CW complexes and not just finite ones. You can find the main results inCubical.CW.Homology
FYI, I also introduced a new definition of < on the naturals and used a definition of Fin n in terms of it. I would suggest we use this as the primary definition of Fin n in the future as the original one caused several of the proofs in this PR to be ~3 times as long (transport hell). But let's leave that to a future discussion...