H-spaces

Stream: maths

[Filippo A. E. Nuccio]

If someone wants to have a look at #16029 it would be really great. There is the definition of H-spaces and the proof that the path space is a H-space, and thanks to a lot of work and great comments by @Junyan Xu I think that the PR looks almost ready to go.