Reduced cohomology+Eilenberg-Steenrod axioms

[aljungstrom]

This PR contains:

1. Reduced cohomology with arbitrary group coefficients
2. A proof that this theory satisfies the Eilenberg-Steenrod axioms

[rwbarton]

I think the definition of coHomTheory should also have fields Hmap_id and Hmap_const, right?
Perhaps you want to add them and their proofs for ordinary cohomology in this PR also?

[aljungstrom]

I think the definition of coHomTheory should also have fields Hmap_id and Hmap_const, right? Perhaps you want to add them and their proofs for ordinary cohomology in this PR also?

Wups! Thanks for pointing this out. I'll fix it in a separate PR as soon as Anders merges this one (and the Gysin one since it depends on this one).

[felixwellen]

Same here. It still checks on current master, if you change "--experimental-lossy-unification" to "--lossy-unification".

[felixwellen]

Great stuff - I only have organisational comments and one fix.

[mortberg]

@aljungstrom Can you fix @felixwellen's comments and then we can merge?

We should not forget to add the missing fields that @rwbarton pointed out as well

[mortberg]

Merging this now.

@aljungstrom please make a new PR adding the two missing fields from coHomTheory (functoriality for Hmap) and necessary proofs for the cohomology theories we have