fact: Definition group_to_oogroup : Group -> ooGroup := fun G => Build_ooGroup (pClassifyingSpace G) _.
imports: Basics Types Pointed Truncations.Core Truncations.Connectedness Homotopy.ClassifyingSpace Algebra.Groups WildCat