fact: Definition group_loops_functor_idmap {X : pType} : grouphom_idmap (group_loops X) == group_loops_functor (Id (A:=pType) _).
imports: Basics Types Pointed Truncations.Core Truncations.Connectedness Homotopy.ClassifyingSpace Algebra.Groups WildCat