Build_AbGroup' (G : Type) `{Zero G, Negate G, Plus G, IsHSet G} (comm : Commutative (A:=G) (+)) (assoc : Associative (A:=G) (+)) (unit_l : LeftIdentity (A:=G) (+) 0) (inv_l : LeftInverse (A:=G) (+) (-) 0) : AbGroup. Proof. snrapply Build_AbGroup. - rapply (Build_Group G). repeat split; only 1-3, 5: exact _. + intros x. lhs nrapply comm. exact (unit_l x). + intros x. lhs nrapply comm. exact (inv_l x). - exact comm. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.