Define Universal Property for Algebraic Structures

[felixwellen]

There are lot's of universal properties in the algebra part of the library and we often use easy consequences of those, e.g. uniqueness of universal things. Unfortunately, it is not possible to use a definition from category theory, since that wouldn't be general enough in terms of universe levels. So it probably makes sense to have a specific definition for algebraic structures. This, however, could mean redefining some category theory with more general universe levels...

[maxsnew]

Why wouldn't the definition from category theory be general enough?