agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
Introducing a new folder that, so far, defines quasigroups and loops (unital quasigroups).
For roughly the same reason as topologists like, say, Hausdorff groups, constructive algebraists like working with gadgets where the underlying set has a tight apartness relation. Examples in nature include...
[Type duality](https://unimath.github.io/agda-unimath/foundation.type-duality.html) talks about a natural transformation between a covariant functor and a contravariant one, which doesn't make sense. We are really talking about the contravariant functor that has the...
The smash product is the pushout of the half smash products ```text X ×∗ Y -----> X ⋊∗ Y | | | | ∨ ⌜ ∨ X ⋉∗ Y ----->...
It seems a bit useless to be inserting links to people every place they're mentioned when this information is already stored in `contributors.toml`. It would be useful to be able...
Freek's list is weird and arbitrary, and although it is widely used as a benchmark by libraries of formalized mathematics and therefore it is important to track it on our...
Should we consider setting the `--lossy-unification` flag globally for the library? Degrading performance due to not enabling this flag is a recurring issue that new contributors face and lose a...
This issue is particularly noticeable in the main module headers:
The readability of formalizations on our web page suffers on mobile devices in part due to excessive margins. Could we do something to reduce these margins? **Side note.** While testing,...