Build_IsSubgroup' {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)) : IsSubgroup H. Proof. refine (Build_IsSubgroup G H _ unit _ _). - intros x y. intros hx hy. pose (c' := c mon_unit y). specialize (c' unit). specialize (c x (-y)). rewrite (negate_involutive y) in c. rewrite left_identity in c'. apply c. 1: assumption. exact (c' hy). - intro g. specialize (c _ g unit). rewrite left_identity in c. assumption. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.