Cavallo's trick for H-spaces

[fredrik-bakke]

No description provided.

[fredrik-bakke]

This PR is ready for merging now IMO. I might look over it again in the beginning of next week and if so merge it, if that is alright @VojtechStep.

I'm not currently happy with the construction of coherence-point-htpy-map-Ω which is why it is abstract. There should be a neater way to do it by defining the appropriate lemmas for tr-Ω, but I leave that for future work.

[VojtechStep]

I'm not currently happy with the construction of coherence-point-htpy-map-Ω which is why it is abstract.

Then please say so in the code. It's inconvenient to look for decisions like this on GitHub.

[fredrik-bakke]

Then please say so in the code. It's inconvenient to look for decisions like this on GitHub.

Good point, Ive done so now

[fredrik-bakke]

😮 Thanks for approving!