Hurewicz theorem for CW complexes

[aljungstrom]

Sorry, huge PR incoming... The code in this PR is ported from a private repo containing the formalisation of (most of) Cellular Methods in Homotopy Type Theory by me and @loic-p. Since it also contains results that'll be used in the Serre Finiteness formalisation (ping @owen-milner, @rwbarton, @mortberg), I think it belongs in the cubical library.

Key results:

1. The Hurewicz theorem.: HurewiczTheorem in Cubical/CW/HurewiczTheorem.agda
2. Homotopy groups of sufficiently connected CW complexes are finitely presented:
   isFinitelyPresented-π'connectedCW in Cubical/CW/Connected.agda
3. Pushout structure on CW complexes: in Cubical/CW/Instances/Pushout.agda

Detailed overview:

Cubical/Algebra/...

• Finitely presented abelian groups
• other minor missing results

Cubical/CW/...

• Cellular approximation theorem (for finite CW complexes), (Approximation.agda)
• Renamings (e.g. isCW -> hasCWskel)
• Characterisation of low-dimensional structure of n-connected CW complexes (Connected.agda)
• Computations of homology groups of some important spaces (Groups/...)
• Hurewicz theorem (HurewiczTheorem.agda)
• CW structure on key constructions such as empty types, pushouts, joins, etc. (Instances/...)
• Construction of CW complexes and maps with certain strict equalities (Strictification.agda)

Cubical/Data/...

• Other minor results

Cubical/HITs/...

• 'Abelianised' path types and their theory (path types with an additional constructor forcing commutativity of path composition). These are used to compute abelianised fundamental groups directly via encode-decode proofs (AbPath/...)
• Basic results about maps bouquets, pushouts and sequential colimits, sphere bouquets, suspensions and wedge sums.

Cubical/Homotopy/...

• Connectedness of wedge inclusion (BlakersMassey.agda)
• Minor results/constructions concerning connectedness and homotopy groups
• Computation of homotopy groups of Sphere bouquets (Group/PiSphereBouquet.agda)
• Computation of homotopy groups of cofibres of maps between Sphere bouquets (Group/PiCofibFinSphereBouquetMap.agda)
• Computation of abelianised homotopy groups of cofibres of maps between Sphere bouquets (Group/PiAbCofibFinSphereBouquetMap.agda)

[mortberg]

Just some very minor things. Amazing stuff!

[rwbarton]

You can remove {-# OPTIONS --safe #-} from each module since it's now set globally in the .agda-lib file.