This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
View the Project on GitHub UniMath/UniMath
Generalities about groups G acting on sets, including the structure identity
principle. Definition of torsor. Definition of BG and its covering space EG.
Proof (using univalence) that the loop space of BG is G.