fact: Definition grp_homo_loops {X Y : pType} `{IsTrunc 1 X} `{IsTrunc 1 Y} : (X ->** Y) ->* [LoopGroup X $-> LoopGroup Y, grp_homo_const].
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple