Mukul Agarwal UniMath and Coq

Coq in a HurrySoftware Foundations

In summer 2024, I was fully funded to attend the School on Univalent Mathematics at the University of Minnesota. The school focused on univalent foundations, an approach to the mathematics based on type theory and Voevodsky’s “univalence axiom” (instead of the more familiar Set Theory). Participants worked with UniMath, a library of mathematics formalized in the Coq proof assistant. Since the school used Coq, I learned it beforehand so I could follow the material and work with computer-checked proofs.

I worked through Yves Bertot’s Coq in a Hurry and Benjamin Pierce et al.’s Logical Foundations¹ (my work is located in the repositories linked above).

I especially enjoyed the interplay between learning the mathematics and learning how to express it formally. The summer gave me a starting point for further work with proof assistants and an interest in contributing to UniMath.

Note (added 2026). Coq has since been renamed Rocq; I use the name Coq here to reflect the tools and materials I worked with in 2024.