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. Proof. refine (Build_Subgroup G H _). rapply Build_IsSubgroup'; assumption. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.