Niels van der Weide
Niels van der Weide
This discussion came up twice: - https://github.com/UniMath/UniMath/pull/1432#discussion_r776996433 - https://github.com/UniMath/UniMath/pull/1453#discussion_r804739418 As said by @rmatthes , it would be good to have a global discussion about their respective (dis)advantages. It might also...
If I run `make sanity checks` on my laptop (Mac OS 12.2.1), I get ``` --- checking the ordering prescribed by the files UniMath/*/.packages/files --- make: *** skipping checking the...
At every UniMath school, there was an exercise, which was about showing that the usual definition of the Kleisli category does not give rise to a univalent category. In this...
The compile times are due to some changes I had to make for this package to work with the recent changes in UniMath. If I recall correctly, the definitions for...
Due to a bug in Coq, some coercions were automatically reversible even though they should not have been according to the specification (https://github.com/UniMath/UniMath/pull/1850). For this reason, some coercions are reversible...
What do people think of adding a new package called 'OrderTheory' whose contents are as follows: - The Lattice folder (https://github.com/UniMath/UniMath/tree/master/UniMath/Algebra/Lattice) - The DCPOs folder (https://github.com/UniMath/UniMath/tree/master/UniMath/Combinatorics/DCPOs) - The Posets folder...
The file https://github.com/UniMath/UniMath/blob/master/UniMath/Bicategories/PseudoFunctors/DisplayedUniversalArrow.v should be moved to the directory `DisplayedBicats`, because it is about displayed gadgets.
It is becoming too big, and it should be split into smaller independent files.
This suggestion is inspired by a discussion on the UniMath Zulip. It can be confusing for newcomers to use UniMath, because there are some differences between UniMath and plain Coq...
In UniMath, we use the terminology 'power_category' for a product of categories over a type: https://github.com/UniMath/UniMath/blob/7d0cf5acb3388aaab5cfa4b457d5e8f63b979ec6/UniMath/CategoryTheory/ProductCategory.v#L88 This came up in https://github.com/UniMath/UniMath/pull/1633#discussion_r1121696020. Personally, I am not too fond of that terminology....