Theorems for universal property

[zwang123]

Will mark this ready once #5015 is merged and merge conflict is resolved.

[tirix]

It's really interesting to see a formalization of universal properties!
There are several objects which could (also) be defined in terms of universal properties, it would really be interesting to see universal properties in action.

[zwang123]

It's really interesting to see a formalization of universal properties! There are several objects which could (also) be defined in terms of universal properties, it would really be interesting to see universal properties in action.

I observe tensor product being defined with a universal property in a textbook but I guess it would only generate an equivalence class if it were used as the definition in metabox. Still a good property to prove that some objects have! Also sometimes I think we want the equivalence class to be defined, in which case it could work in definition.