fact: Definition LoopGroup (X : pType) `{IsTrunc 1 X} : Group := Build_Group (loops X) concat idpath inverse (Build_IsGroup _ _ _ _ (Build_IsMonoid _ _ _ (Build_IsSemiGroup _ _ _ concat_p_pp) concat_1p concat_p1) concat_Vp concat_pV).
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple