Niels van der Weide
Niels van der Weide
The whiskered style of monoidal categories is now the standard notion for which infrastructure will be developed. However, some files do not adhere to this yet. - [ ] https://github.com/UniMath/UniMath/tree/70f0cd4e03cbc888b796bb0f6744f59956f8855a/UniMath/CategoryTheory/Monoidal/RezkCompletion...
Currently, the folder https://github.com/UniMath/UniMath/tree/70f0cd4e03cbc888b796bb0f6744f59956f8855a/UniMath/Bicategories/MonoidalCategories is rather disjoint from Bicategories. Some files could be moved to more logical places: To DisplayedBicats/Examples - [ ] https://github.com/UniMath/UniMath/blob/70f0cd4e03cbc888b796bb0f6744f59956f8855a/UniMath/Bicategories/MonoidalCategories/ActionsFormBicategory.v - [ ] https://github.com/UniMath/UniMath/blob/70f0cd4e03cbc888b796bb0f6744f59956f8855a/UniMath/Bicategories/MonoidalCategories/BicatOfActegories.v - [...
- [ ] No notion of oplax functor is defined - [ ] Monoidal dialgebras should use a lax functor and an oplax functor instead of a lax and a...
In several files, either the command `Set Kernel Term Sharing.` or `Unset Kernel Term Sharing.` is used (https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:flag.Kernel-Term-Sharing). I have a couple of questions: - What does this command do...
We have the following in the style guide: > Always use Coq's proof structuring syntax ( { } + - * ) to focus on a single goal immediately after...
This PR contains: - definition of enriched profunctors - unitors and associators - whiskering operation It also develops the infrastructure necessary for these operations. I also fixed a mistake that...
This PR finishes the tripos to topos construction. The missing parts were subobject classifiers and exponentials, and these are finished now. I also added a concrete instantiation of the tripos...
Coq 8.20 is out (yay!). I am currently compiling UniMath with Coq 8.20, and we get some new warnings about notations and their priorities (there also is an unnecessary print...
Sorry for the large PR. This PR collects the main research I did during summer. The content of this pull request is as follows: - A biequivalence between categories with...
This is taken from @fredrik-bakke, and the explanation is as follosw Clause by clause: - `github.event_name == 'workflow_dispatch'`: the job will run if it was manually dispatched. - `github.event_name ==...