The powerset is not universe polymorphic enough

[anshwad10]

Currently, for A : Type l, ℙ A is defined as A -> hProp l, however I frequently find myself needing to use A -> hProp l' where l' is greater than the universe level of A. I could use Embeddings instead which are maximally universe polymorphic, however I run into a problem: Subset→Embedding use ℙ, so I can't use that without compromising the universe polymorphism. Also, this causes more problems in the rest of the library: for example, subgroups and ideals are not maximally universe polymorphic because they use ℙ, and neither is ΣPropCat (though that is redundant because of FullSubcategory and should be removed anyways). I see two solutions to this:

• Define an alternate version ℙ' and use that whenever the extra universe polymorphism is needed
• Modify the definition of ℙ to take another universe level argument; This would be a breaking change and would require editing a lot of the library

Thoughts