This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
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.