[Draft] working on dcpo presentations #120
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jonsterling
changed the title
Only regularizing the formatting of the code we are adding; this file needs attention/cleanup in a separate PR.
jonsterling
commented
Feb 25, 2023
| where | ||
|
|
||
| Cover-set : 𝓤 ⊔ 𝓥 ⁺ ⊔ 𝓦 ⁺ ̇ -- This one has spurious assumptions | ||
| Cover-set = G → {I : 𝓥 ̇} → (I → G) → Ω 𝓦 |
There was a problem hiding this comment.
I am wondering whether this is a workable way to formulate the set of covers in a univalent setting. In particular, I think we would need it to be a family of types rather than a family of propositions. But maybe there is some better formulation anyway.
There was a problem hiding this comment.
There are two powersets in the original definition. I changed the inner one but not the outer one, because I was not so sure about how the outer one is used.
|
Any progress with this? |
|
I'm about to come back to this as summer holiday is coming. |
|
Is there an intention to continue this work? |
|
@jonsterling @Trebor-Huang Do you plan to finish this? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a draft PR containing @Trebor-Huang's work on exploring dcpo presentations, roughly following Jung, Moshier, and Vickers. We will mark it as such when it is ready for review, but preliminary feedback is welcome along the way at any time.