The agda-unimath library is a community formalization project for univalent
mathematics in Agda. The library project was
created by Elisabeth Bonnevier, Jonathan Prieto-Cubides, and Egbert Rijke, and
is also being maintained by Fredrik Bakke. Our goal is to formalize an extensive
curriculum of mathematics from the univalent point of view. Furthermore, we
think libraries of formalized mathematics have the potential to be useful, and
informative resources for mathematicians. Our library is designed to work
towards this goal, and we welcome contributions to the library about any topic
in mathematics.
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|