agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
We should have a list of publications that are formalized in the library. This would be good for exposition, would give new readers some pointers for what to read in...
I noticed today that on our website the search functionality seems to give 15 results only. That would be a great choice if the search functionality would be very good...
We have a growing collection of metafiles that are polluting the root folder of the repository. I think it would be best if we moved them to a subdirectory. This...
The `elementary-number-theory` module is in need of some love and attention. This issue is not aiming for a complete overhaul as one might be tempted to, but I will record...
### Real numbers - [ ] Factor out lower and upper Dedekind cuts into their own files. - [ ] lower and upper Dedekind reals should probably be their own...
We have a GitHub action for typechecking the library with performance tracking on master, but it would be nice to know what impact a PR has before merging it, so...
The font size in agda code blocks is larger than in other code blocks. Inspection reveals that Agda code is displayed with a font size of 15.68px, while text blocks...
## The cd-excision project ### Project description A **complete cd-structure** consists of a class of **distinguished squares** of maps, i.e., distinguished morphisms in the arrow category, that is stable under...
Currently, the library is blocked from enabling the `--level-universe` option globally due to a single definition, namely `telescope`. Although `telescope` is a very useful construction, having `--level-universe` enabled is also...
This is useful because it can give definitional computation laws for the inverse. It will take a large effort to refactor the greater library, but perhaps it is possible to...