agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
Defines unbounded π-finite types and repeats the proofs that are already done for π-finite types. This includes - Unbounded π-finite types are closed under equivalences and retracts. - Truncated π-finite...
The library still appears in this less-than-favorable form in Google's search results: There's a few issues to point out that could be improved. 1. The site title is "Github Pages"...
> I agree that the way we display/handle references is not the best way. It's probably a good idea to take some inspiration from $n$Lab. While they're probably not entirely...
Refactoring the metric space module (#1421) - remove the notion of `Premetric` / `Premetric-Space`; - all (pseudo)metric spaces are saturated; - simplify hierarchy in concepts (define things for for metric...
Recent contributions in the `metric-spaces` modules raise concerns about the names of some concepts in the `metric-spaces` module. # TODO - [ ] The divide metric space/metric structure seems a...
This PR introduces the notion of `Metric-Semigroup`, metric spaces with a short associative binary operator. Credit @lowasser for https://github.com/UniMath/agda-unimath/pull/1447/commits/9e36ee4cb60533a860a03b784fda0145abbf31da
The next version of Agda features a new "main mode" `--build-library` for building libraries, making the `src/everything.lagda.md` entry point superfluous. When this version releases, we should move to using this...
This PR standardizes pullbacks in `category-theory` with standard pullbacks in `foundation` and dualizes them to get pushouts matching pushouts in `synthetic-homotopy-theory`.
