agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
Detected in #1025 when I tried having files including the string `large-wild-⟨0,1⟩-precategories.lagda.md` in their name.
This PR adds the following files to the library: - Foundation - Symmetric cores of binary relations - Graph Theory - The forgetful functor from directed graphs to undirected graphs...
Construct the hopf fibration in such a way that the generator of $\mathbb{S}^3$ is sent to a 3-loop in $\mathbb{S}^2$ constructed using Eckmann-Hilton. A detailed plan for this may be...
The following is an excerpt from [`DESIGN-PRINCIPLES.md`](https://unimath.github.io/agda-unimath/DESIGN-PRINCIPLES.html): > Note that there is some redundancy in the postulates we assume. For example, the [univalence axiom implies function extensionality](https://unimath.github.io/agda-unimath/foundation.univalence-implies-function-extensionality.html), but we still...
A recent update to pre-commit or Python led to breaking changes for the autoformatting functionality for Python files, so I had to disable them in #701. However, such functionality would...
This issue outlines formalization goals for the `category-theory` module. ### Formalization targets The following list outlines missing formalizations that should be part of any standard library on category theory: -...
This seems appropriate following the discussion with Anders after #910 that "properties", of categories should be separated from its "data", and allows us to repeat fewer arguments.
Hi, I would like to finish my initial goal about cardinalities in Set Theory directory. It means the completion of Section 10.2 of HoTT book. I just need to remember...
This PR refactors the graph theory library with updates from the Beyond Finite Sets PR.