Fredrik Bakke’s fork of the agda-unimath library

Welcome to my personal fork of the agda-unimath project. See “Recent changes” below to see what I’ve been recently up to.

🚧 This fork/website is currently under reconstruction. 🚜

This library is compatible with Agda 2.8.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.

I do not currently accept contributions, but feel free to contact me via my academic contact details.

Recent changes

• 2026-04-02. Fredrik Bakke. update front materials.
• 2026-04-02. Fredrik Bakke. change/fix benchmark publishing workflow.
• 2026-04-02. Fredrik Bakke. change publishing url.
• 2026-04-02. Fredrik Bakke. # Disable “Content created by” attribution everywhere.
• 2026-04-02. Fredrik Bakke. update goatcounter.
• 2026-03-23. Vojtěch Štěpančík. Add a Random Module button (#1918).
• 2026-03-22. Louis Wasserman. The large precategory of vector spaces (#1919).
• 2026-03-22. Louis Wasserman. Invertible elements in large monoids (#1865).