agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
The file simpson-delooping-sign-homomorphism does not compile with --experimental-lossy-unification
It runs into universe problems, indicating that there is something off with the file. Some lemmas are extremely long, and it is also one of files that takes longest to...
There are certain molecules called allotropes of carbon which consist entirely of carbon atoms. Examples include carbon nanotubes and fullerines. https://en.wikipedia.org/wiki/Allotropes_of_carbon https://en.wikipedia.org/wiki/Carbon_nanotube https://en.wikipedia.org/wiki/Fullerene With the current definition of hydrocarbon, these...
Benzene is a molecule with 6 carbon atoms and 6 hydrogen atoms, where the carbon atoms are arranged in a manner such that the projection into 2-dimesnional space is a...
### TODO - [ ] #714 - [ ] Clean up commented code - [x] Clean up unused imports (?) - [x] #479 - [x] Add symbol for coproducts -...
TODO - [ ] Prove that `mono-Concrete-Group` is a set. - [ ] Define the type of subgroups using G-sets. - [ ] Prove that the two types are equivalent....
- Large and small noncoherent wild $(∞,∞)$-precategories - maps of globular types - maps of noncoherent wild $(∞,∞)$-precategories - Colax functors of noncoherent wild $(∞,∞)$-precategories - Induced colax functor on...
WIP https://github.com/UniMath/agda-unimath/issues/1043
_This is an experiment_ The motivation for this PR is merely that I am curious what the library will look like if we wouldn't have postulates. This pull request is...