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

Additions to the Powerset module #1056

Draft
wants to merge 10 commits into
base: master
Choose a base branch
from
Draft

Additions to the Powerset module #1056

Changes from 1 commit
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
a4e2c07
Update Powerset module
rahulc29 Sep 15, 2023
17a44f2
Make repeated definition private
rahulc29 Sep 15, 2023
e2f60ee
Remove unnecessary using
rahulc29 Sep 15, 2023
a93a782
Merge branch 'agda:master' into master
rahulc29 Nov 1, 2023
5723634
Merge branch 'agda:master' into master
rahulc29 Nov 3, 2023
3359f1c
Merge branch 'agda:master' into master
rahulc29 Nov 13, 2023
f500c04
Merge branch 'agda:master' into master
rahulc29 Mar 23, 2024
de0a479
Sync with agda/cubical
rahulc29 Mar 23, 2024
d4ca6fa
Add preorder structure on the category of subobjects
rahulc29 Mar 23, 2024
2c018ad
Merge branch 'agda:master' into master
rahulc29 Mar 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cubical/Foundations/Powerset.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ private data _⊎_ (A B : Type ℓ) : Type ℓ where
inr : B → A ⊎ B
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think it's a good idea to have two versions of a datatype, especially since they are not definitionally equal. It would be better to split Cubical.Data.Sum into Cubical.Data.Sum.Base and .Properties, import sum from .Base, and have .Properties import from Embeddings so there is no circular dependency and no duplication. (And I don't think making it private fixes it: How does a user of this library give an element of A U B without being able to access the constructors of the datatype underlying it?)


-- Repeated from Cubical.Functions.Logic
∥_∥ₚ : (X : Type ℓ) → hProp ℓ
private ∥_∥ₚ : (X : Type ℓ) → hProp ℓ
∥ X ∥ₚ = ∥ X ∥₁ , squash₁

-- Binary Unions
Expand Down