Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Additions to the powerset module #1052

Open
5 tasks done
rahulc29 opened this issue Sep 14, 2023 · 2 comments · May be fixed by #1056
Open
5 tasks done

Additions to the powerset module #1052

rahulc29 opened this issue Sep 14, 2023 · 2 comments · May be fixed by #1056

Comments

@rahulc29
Copy link
Contributor

rahulc29 commented Sep 14, 2023 •
edited
Loading

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
Copy link
Collaborator

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

@rahulc29 rahulc29 linked a pull request Sep 15, 2023 that will close this issue
Draft
@rahulc29
Copy link
Contributor Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Additions to the Powerset module rahulc29/cubical
2 participants
@mortberg @rahulc29