Unimath

Unimath is a Rocq library that formalizes univalent mathematics

References