CW complexes, cellular homology + a lot more

[aljungstrom]

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:

1. Definitions of CW complexes, (finite) cellular maps and (finite) cellular homotopies. This includes things like (constructive versions of) the cellular approximation theorems. All of this can be found under Cubical.CW.
2. Chain complexes, chain homotopies and related constructions. We use finite counterparts of many of these constructions to keep things constructive.
3. Construction of the chain complex associated to a CW complex à la Buchholtz and Favonia. This includes a bunch of proofs concerning properties of the degree of (1) maps between spheres (2) maps between bouquets of spheres.
4. Perhaps most importantly: cellular homology and, in particular, its functoriality. Actually, this is concerns two homology theories: we first construct Hˢᵏᵉˡ which defines the homology of an explicitly given skeleton and then lift this to Hᶜʷ, 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 in Cubical.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...

[aljungstrom]

@rwbarton @owen-fool maybe this is of interest to your formalisation project?

[rwbarton]

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?

[aljungstrom]

@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.

[mortberg]

Cool stuff! Some minor comments