-
Notifications
You must be signed in to change notification settings - Fork 68
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.
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
Basic properties of the flat modality #1078
Conversation
I am marking this PR as ready for review, as it is very close to finished. What I have in mind left to complete are a couple of sections of prose that I have specifically tagged with |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have reviewed the changes to foundation
, foundation-core
, and elementary-number-theory
so far, which seem to have little to do with basic properties of the flat modality. I will review the other changes later.
src/foundation-core/postcomposition-dependent-functions.lagda.md
Outdated
Show resolved
Hide resolved
src/foundation-core/postcomposition-dependent-functions.lagda.md
Outdated
Show resolved
Hide resolved
src/foundation-core/postcomposition-dependent-functions.lagda.md
Outdated
Show resolved
Hide resolved
Co-authored-by: Egbert Rijke <[email protected]>
Would it be reasonable a separate PR for the changes not in One way to do this is:
Note that this is only a suggestion. If you prefer to not create a separate pull request for these changes, that's ok with me too. |
Yes! I was thinking the same actually. 😅 |
Btw if there is a better way to do this, I would love to know. This was just the one way I know how to create a branch with changes from specific folders, but obviously my |
That's not true. I didn't for instance know how to do this before you instructed me just now. |
I've added the missing explanations mentioned in this comment now. |
Extracts changes made in #1078 to parts of the library outside of `modal-type-theory`.
Since it seems no one is willing to give a review of this PR, I'm happy to have it merged without one. If that is okay with you @EgbertRijke @VojtechStep |
I quickly glanced over this PR and it looks good to me. Sorry that this flew under the radar for so long. |
This is the replacement of #1005.
Proves a series of basic properties of the flat modality.
Summary
General properties
The dependent universal property of flat discrete crisp typesLeft exactness of flat
Flat distributes over sequential limitsRight exactness of flat
Flat distributes over pushoutsFlat distributes over coequalizersFlat distributes over sequential colimitsNotes
cons-flat
tointro-flat
. This makes it easier to distinguish fromcounit-flat
.crisp-based-ind-Id
from the existence of the sharp modality rather than postulating it. The same is true for the modal induction principle of the sharp modality.