Univalent Mathematics
Univalent Mathematics
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
agda-unimath
The agda-unimath library
Foundations
Voevodsky's original development of the univalent foundations of mathematics in Coq
SymmetryBook
This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
TypeTheory
The mathematical study of type theories, in univalent foundations