search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Additions to the powerset module #1052

Open rahulc29 opened 11 months ago

rahulc29 commented 11 months ago

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

  1. [x] A ∈ₚ operator that produces an hProp for x ∈ₚ A rather than a general type
  2. [x] Binary unions and intersections
  3. [x] Indexed unions and intersections
  4. [x] A separate type for "inhabited subsets"
  5. [x] 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 commented 11 months ago

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

rahulc29 commented 11 months ago

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