proposition: Lemma equiv_grp_hfiber {A B : Group} (f : GroupHomomorphism A B) (b : B) : forall (a0 : hfiber f b), hfiber f b <~> hfiber f mon_unit.
proof: Proof. intros [a0 p]. refine (equiv_transport (hfiber f) (right_inverse b) oE _). snrapply Build_Equiv. { srapply (functor_hfiber (h := fun t => t * -a0) (k := fun t => t * -b)). intro a; cbn; symmetry. refine (_ @ ap (fun x => f a * (- x)) p). exact (grp_homo_op f _ _ @ ap (fun x => f a * x) (grp_homo_inv f a0)). } srapply isequiv_functor_hfiber. Defined.
imports: Basics Types HProp HFiber HSet PathAny (notations) Classes.interfaces.abstract_algebra (hints) Classes.interfaces.abstract_algebra (hints) Classes.interfaces.canonical_names Classes.interfaces.canonical_names (SgOp, sg_op, One, one, MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity, Negate, negate, Associative, simple_associativity, associativity, LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity) Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, negate_l, negate_r, IsSemiGroup(..), sg_set, sg_ass, IsMonoid(..), monoid_left_id, monoid_right_id, monoid_semigroup, IsMonoidPreserving(..), monmor_unitmor, monmor_sgmor, IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit) Classes.theory.groups Pointed.Core WildCat Spaces.Nat.Core Truncations.Core