{A B : Group} (f : GroupHomomorphism A B) (b : B) : forall (a0 : hfiber f b), hfiber f b <~> hfiber f mon_unit. 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.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.