github.com/UniMath/UniMath ↗
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
Open this visualization on its own page →
Contributors
71
Lines of Code
18,980
From
2010-10-04
To
2021-01-05
About UniMath/UniMath
UniMath is a substantial formalized mathematics library written in Rocq (formerly known as Coq), designed to encode mathematics from the perspective of univalent foundations. The univalent approach treats mathematical structures as fundamentally based on equivalence rather than strict equality, offering a different foundational viewpoint for formalizing mathematics compared to traditional set-theoretic approaches.
The library provides comprehensive tools for mathematical formalization covering multiple areas of mathematics. It includes extensive documentation, tutorials, and educational materials, with interactive browser-based environments for experimentation. UniMath also offers multiple ways to explore and understand the codebase through automatically generated documentation in both alectryon format (which allows stepping through proofs with visible goals) and rocqdoc format (which enables navigation through mathematical definitions and theorems).
The project maintains an active community supported through a Zulip chat for questions and discussions, with regular engagement around installation, usage, and development. UniMath is designed to be accessible to both researchers working in formal mathematics and students learning about univalent foundations and proof assistants, with organized schools and educational resources available alongside the core library.