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.
By inserting
Set Printing Universes. About Sets.on line 86 ofInstance/Sets.vone can check, that according to Coq the universeso, h, sh, pin the definition ofSetsall need to be equal. I observed this with Coq v8.17 and the master branch. The patch removes the universe variablesh, sh, pfrom the signature ofSetsand substitutes them witho. This should makeSetsa bit easier to understand and use, when explicit universes are needed.The changes to
Adjunctionare there to deal with the new definition. One universe variable could be removed, because it only occurred as argument toSets.I am not entirely sure how the equalities arise. By using
Aboutsome more I found the following (forSets@{o h so sh p}):Categoryforcessh ≤ pobj := SetoidObjectforceso, p < soSetoidMorphismforceso ≤ pando = h.SetoidMorphism_Setoid@{o h p}forceso = h = p.Similar equations arise in other definitions, but I do not use these as much as
Sets.