Basic properties of the flat modality #1005
Closed
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
|
whoops, turns out renaming branches closes PRs 😅 |
Pre-commit tries to run a downloaded NodeJS executable when NodeJS isn't available in the environment, but that fails to run on NixOS.
…niMath#1052) ### Summary - Refactors the definition of categories to use the new and more general strictly involutive identity types for their associativity witnesses. - Refactor definitions of some instances of large and small precategories to use a new `make-(Large-)?-Precategory` constructor. - Defines the underlying large precategory of a large subprecategory. - Change some prose regarding basic definitions in category theory. - Refactors all appropriate instances of large precategories to be (full) large subprecategories. - Rename `is-group` to `is-group-Semigroup`. The last item was appropriate to make the handling of `involutive-eq-associative-comp-hom-***-Large-Precategory` systematic. Improves on what was implemented in UniMath#945.
Adds citation support using a biblatex file and [pybtex](https://pybtex.org/), reactors most current citations to use it, and adds a small guide to explain how to use it. Resolves UniMath#957.
…h#1066) I found two instances where the concepts macro wasn't formatted properly, so I added a check to the preprocessor that fails the website build. This means that the preprocessor will run in full for the `linkcheck` output. We could have it only do some of the work for just checking if all the tags are well-formatted, but most of the time is still spent in IO with the `mdbook` process, which we can't speed up.
The changes in this PR are pulled from UniMath#885.
The concept macro looks for Agda definitions when the Agda= component is specified. Until now the definition name was not escaped, so concepts like the coproduct type `_+_` could not be found by the macro. Fixes UniMath#1073
…type-families` (UniMath#1065) This PR moves the torsoriality of the identity types to `foundation-core.torsorial-type-families`. Previously it was in `contractible-types`. I also slightly updated the prose, and fixed imports wherever they were broken because of this move.
18 tasks
|
This PR is succeeded by #1078 due to merging issues. |
EgbertRijke
pushed a commit
that referenced
this pull request
Sep 6, 2024
This is the replacement of #1005. Proves a series of basic properties of the flat modality. ## Summary ### General properties - [X] The universal property of flat discrete crisp types - [x] ~The dependent universal property of flat discrete crisp types~ - [X] Functoriality of flat - [X] Flat is idempotent - [x] A crisp type is crisply flat discrete if its counit has a crisp section ### Left exactness of flat - [X] Flat distributes over identity types - [X] The crisp identity types of flat discrete crisp types are flat discrete - [X] Flat distributes over dependent pair types - [X] Flat distributes over product types - [x] Flat distributes over pullbacks - [x] ~Flat distributes over sequential limits~ - [x] The unit type is flat discrete ### Right exactness of flat - [X] The empty type is flat discrete - [X] The natural numbers are flat discrete - [X] Flat distributes over coproduct types - [x] ~Flat distributes over pushouts~ - [x] ~Flat distributes over coequalizers~ - [x] ~Flat distributes over sequential colimits~ ### Notes - The constructor for the flat modality is renamed from `cons-flat` to `intro-flat`. This makes it easier to distinguish from `counit-flat`. - In the future, we will probably want to prove `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. - This PR does some ground work with the sharp modality too.
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.
Proves a series of basic properties of the flat modality.
Summary
General properties
Left exactness of flat
Right exactness of flat