This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
This Rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
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.
See the documentation for general information about UniMath, install instructions, guides, tutorials and information about contributing.
See also the automatically generated alectryon documentation, where you can step through the proofs, viewing the goals at every step, and the the rocqdoc documentation, where you can click on identifiers (like disp_cat
) to go to their definition. By replacing rocqdoc
with alectryon
in the url and vice versa, you can switch between the rocqdoc and alectryon documentation.
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.