Cleaning up for homotopy groups

[EgbertRijke]

In anticipation of #834 I thought I'd clean up some stuff around homotopy groups and define them in a way that is well-connected with the existing formalization of groups, concrete groups, and higher groups.

[fredrik-bakke]

Could we try and get this PR merged (or closed) @EgbertRijke? I'd be happy to wrap it up for you since you are not prioritizing it, but it seems unfortunate to me that this PR is so to speak "squatting" on the concept of homotopy groups, when it seems to me that other contributors are also interested in writing contributions about homotopy groups.

[EgbertRijke]

Could we try and get this PR merged (or closed) @EgbertRijke? I'd be happy to wrap it up for you since you are not prioritizing it, but it seems unfortunate to me that this PR is so to speak "squatting" on the concept of homotopy groups, when it seems to me that other contributors are also interested in writing contributions about homotopy groups.

I'd be very happy if you'd help me with this pull request. I don't think I'll be working on this within a month from now.

[fredrik-bakke]

I'd be very happy if you'd help me with this pull request. I don't think I'll be working on this within a month from now.

Great! I'll have a look within the week :)

[fredrik-bakke]

Okay, I've fixed merge conflicts and added the definition of a concrete homotopy group, so this PR is ready to be reviewed.