Global function classes #890
Merged
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
|
Whoop-de-do, now you're a co-author on all of my current PRs @VojtechStep 😬 |
|
Uh, that's not ideal - feel free to rebase and change the commit message to delete the co-authored-by line |
|
uhh, how do I do that more concretely? |
|
Or, well, technically you should now rebase on master instead of merging it in your branch, then it would be OK since that commit wouldn't be in the new branch's history difference |
|
If you give me like an hour I'll be at my computer and I'll be able to give more concrete steps |
|
I think I'm doing what you told me, but nothing ends up changing on GitHub :( |
fredrik-bakke
force-pushed
the
global-factorization-systems
branch
2 times, most recently
from
98450b0
to
a27c178
Compare
|
fixed :) |
|
Ohhh, I guess I had to force-push earlier. That clears up a lot of things for me |
|
Man, git-terminology is one of the worst modern inventions. |
Merged
|
Whoops, I think I closed this one by mistake |
EgbertRijke
reviewed
Nov 9, 2023
EgbertRijke
reviewed
Nov 9, 2023
This was referenced Nov 19, 2023
Merged
fredrik-bakke
added a commit
that referenced
this pull request
Nov 24, 2023
### Additions - Module on modal type theory, including - Define the flat modality - Define the sharp modality - Start work on their adjunction - Some basic definitions about codiscrete types and the flat modal operator - Some additions on higher modalities - Introduce (strong) subuniverse induction as a relaxation of modal subuniverse induction - Show we can induct on the identity types with a higher modality without appealing to univalence using strong subuniverse induction - Start on functorial properties of higher modalities - Multivariable sections is a definition of sections of multivariable maps that make it possible to circumvent applying function extensionality in many cases. (If we at some point in the future want a module on simplicial homotopy type theory, then it would be fruitful to develop the module on modal type theory further :)) ### A regression It has become clear that the current formulation of higher modalities is not the most practical one, as it needs to assume everything is sufficiently contained within a single universe. In addition, the small relaxation to locally small types seems somewhat contentless and makes the formalizations more cumbersome. I have started a new line of formalization to fix these problems in #890.
fredrik-bakke
added a commit
to fredrik-bakke/agda-unimath
that referenced
this pull request
Nov 29, 2023
fredrik-bakke
added a commit
to fredrik-bakke/agda-unimath
that referenced
this pull request
Nov 29, 2023
### Additions - Module on modal type theory, including - Define the flat modality - Define the sharp modality - Start work on their adjunction - Some basic definitions about codiscrete types and the flat modal operator - Some additions on higher modalities - Introduce (strong) subuniverse induction as a relaxation of modal subuniverse induction - Show we can induct on the identity types with a higher modality without appealing to univalence using strong subuniverse induction - Start on functorial properties of higher modalities - Multivariable sections is a definition of sections of multivariable maps that make it possible to circumvent applying function extensionality in many cases. (If we at some point in the future want a module on simplicial homotopy type theory, then it would be fruitful to develop the module on modal type theory further :)) ### A regression It has become clear that the current formulation of higher modalities is not the most practical one, as it needs to assume everything is sufficiently contained within a single universe. In addition, the small relaxation to locally small types seems somewhat contentless and makes the formalizations more cumbersome. I have started a new line of formalization to fix these problems in UniMath#890.
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.
Global function classes are function classes defined at each universe level that are closed under pre- and postcomposition by equivalences. (not established terminology)
Depends on #891.Please note that some of the files on factorizations of maps are developed further in what will be a subsequent PR.