fact: Definition grp_iso_g_loopgroup_bg : GroupIsomorphism G (LoopGroup (B G)).
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple