Additions to the powerset module

[rahulc29]

I believe the following additions could be made to the Powerset module :

1. A ∈ₚ operator that produces an hProp for x ∈ₚ A rather than a general type
2. Binary unions and intersections
3. Indexed unions and intersections
4. A separate type for "inhabited subsets"
5. The complement of a subset

While these are easy to define I found consistently needing these and believe others could benefit from it too.

I'd be happy to drop in a PR.

[mortberg]

Sounds good to me! Please go ahead and make a PR

[rahulc29]

Hi, I've opened a PR. Let me know if any changes are necessary.
Thanks!

[anshwad10]

I would also like the powerset to be more universe-level polymorphic: Currently, if A is Type a, then P A is A -> hProp a, even though there are multiple different powersets even up to equivalence from choosing different 'a' in the hProp a. I would like these operations to be defined for all universe levels, not just a, by making P take another universe-level argument.