fact: Definition Build_Subgroup' {G : Group} (H : G -> Type) `{forall x, IsHProp (H x)} (unit : H mon_unit) (c : forall x y, H x -> H y -> H (x * -y)) : Subgroup G.
imports: Basics Types HFiber WildCat.Core Truncations.Core Algebra.Groups.Group TruncType