This Rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
- For questions about the UniMath library and requests for help with installing or using the library, visit the UniMath Zulip (click here to register).
- For bugs and suggestions about improvements, file an issue on GitHub.
You can try out UniMath in the browser by clicking here. For instance, you can run the files from the School on Univalent Mathematics in the browser.
- For general information about UniMath, citing UniMath and the coordinating committee, see the documentation page about UniMath.
- For installing UniMath and other software-related information, see setup.
- For contributing to UniMath, see the documentation about contributing.
The UniMath development team gratefully acknowledges the great work by the Coq development team in providing the Coq proof assistant, as well as their support in keeping UniMath compatible with Coq.