The orbit category of a group

[fredrik-bakke]

Prove that G-sets form a category and define the orbit category of a group.

I am like 80% confident that the definition of the orbit category is correct, so if you can confirm or deny it that would be great :)

Builds on #877 and fixes an erroneous renaming from that PR.

[EgbertRijke]

Very excellent pull request! Thank you for these nice new definitions and for the fixes of the errors that I introduced. I will enable auto-merge on this one.

[fredrik-bakke]

Very excellent pull request! Thank you for these nice new definitions and for the fixes of the errors that I introduced. I will enable auto-merge on this one.

Thanks! Did you confirm my definition of the orbit category?

[EgbertRijke]

I don't know what you mean by confirming a definition:)