Refactor category theory to use strictly involutive identity types

[fredrik-bakke]

Summary

• Refactors the definition of categories to use the new and more general strictly involutive identity types for their associativity witnesses.
• Refactor definitions of some instances of large and small precategories to use a new make-(Large-)?-Precategory constructor.
• Defines the underlying large precategory of a large subprecategory.
• Change some prose regarding basic definitions in category theory.
• Refactors all appropriate instances of large precategories to be (full) large subprecategories.
  • Rename is-group to is-group-Semigroup.

The last item was appropriate to make the handling of involutive-eq-associative-comp-hom-***-Large-Precategory systematic.

Improves on what was implemented in #945.

[fredrik-bakke]

This one's ready for review :)

Don't get fooled by the similar number of additions and deletions, many of them are disjoint.

[fredrik-bakke]

Turns out i had refactored all the definitions I wanted to in this PR, so it is completely ready for review

[fredrik-bakke]

My next planned refactoring (of finite types) depends on this PR, so has to wait until this one has been merged.

[EgbertRijke]

My next planned refactoring (of finite types) depends on this PR, so has to wait until this one has been merged.

What do you want to do with finite types?

[fredrik-bakke]

I want to change how the symbol 𝔽 is used. For instance, Poset-𝔽 should be Finite-Poset.

[fredrik-bakke]

Thanks for the suggestions!

[EgbertRijke]

This PR can be merged when you're done with the comments.

[fredrik-bakke]

Great, thanks