fact: Definition HomotopyGroup_type (n : nat) : Type := match n with | 0 => pType | n.+1 => Group end.
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat