Reduced homology of CW complexes

[loic-p]

The current definition for the homology of CW complexes is missing its 0-dimensional component. There are two ways to define 0-dimensional homology: "standard" homology and reduced homology.

This commit defines reduced homology for CW complexes:

• The chain complex associated to a CW presentation is now augmented with Z in dimension -1 [CW/ChainComplex.agda]
• The chain maps and chain homotopies are extended to work in dimension -1 [CW/Map.agda and CW/Homotopy.agda]
• The definition of homology in [CW/Homology.agda] is now fed the augmented chain complex. I changed the name from Hᶜʷ to H̃ᶜʷ to match the standard mathematical notation.