The agda-unimath library

Welcome to the agda-unimath project. This is a community-driven effort aimed at formalizing mathematics from a univalent point of view using the dependently typed programming language Agda.

The library project was created by Elisabeth Stenholm, Jonathan Prieto-Cubides, and Egbert Rijke, and is currently being maintained by Egbert Rijke, Fredrik Bakke, and Vojtěch Štěpančík. Our goal is to create an online encyclopedia of formalized mathematics containing an extensive curriculum of topics from a univalent point of view. We think libraries of formalized mathematics have the potential to be useful, and informative resources for both working and learning mathematicians. Our library is designed to work towards this goal, and we welcome contributions to the library within any topic in mathematics.

The agda-unimath library is compatible with Agda 2.7.0 and can be compiled by running make check from the root directory of the repository. Learn more about using the library locally in our installation guide.

Participating in the project

If you are interested in contributing to the agda-unimath project, we encourage you to join the conversation in our Univalent Agda discord server. This is a discussion platform shared between the 1Lab, agda-unimath, Cubical Agda, and TypeTopology communities, where we are more than happy to get you started.

To contribute, fork the library and create a separate branch for your work. Follow the instructions in our installation guide to set up the project. After you have completed your formalization, submit it via a pull request. We will review your contribution and work towards incorporating it into the agda-unimath library.