Some universes in Sets are necessarily equal

[Columbus240]

By inserting Set Printing Universes. About Sets. on line 86 of Instance/Sets.v one can check, that according to Coq the universes o, h, sh, p in the definition of Sets all need to be equal. I observed this with Coq v8.17 and the master branch.
The patch removes the universe variables h, sh, p from the signature of Sets and substitutes them with o. This should make Sets a bit easier to understand and use, when explicit universes are needed.

The changes to Adjunction are there to deal with the new definition. One universe variable could be removed, because it only occurred as argument to Sets.

I am not entirely sure how the equalities arise. By using About some more I found the following (for Sets@{o h so sh p}):

• The output type Category forces sh ≤ p
• The line with obj := SetoidObject forces o, p < so
• SetoidMorphism forces o ≤ p and o = h.
• SetoidMorphism_Setoid@{o h p} forces o = h = p.

Similar equations arise in other definitions, but I do not use these as much as Sets.