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

[maxsnew]

Personally, I would update it to be more universe polymorphic. I consider the current design to be an anti-pattern as it forces tedious lifting on library users to recover universe polymorphism.

In the categories part of the library, we only have universe polymorphic definitions of presheaves/presheaf categories: https://github.com/agda/cubical/blob/master/Cubical/Categories/Presheaf/Base.agda#L15

[mortberg]

What if you make it more polymorphic but make the new level argument implicit? Hopefully Agda can infer it in many places and the library won't break so much...

[anshwad10]

Hopefully Agda can infer it in many places

I'm not so sure.. For example ℙ A l and ℙ A l-zero would have the same universe level of l-suc l, so agda would probably not be able to infer what is meant just based on the type. Likely making it implicit would cause a similar situation to what happened with Lift

[anshwad10]

Speaking of, it really irks me that Lift takes j as an implicit argument even though it can rarely be inferred and is always given explicitly anyways. Is there a reason nobody has fixed this, other than it would be annoying task to change all the places where it used? If so, should I open a PR and fix it?