{A : Group} (f : G $-> A) (h : forall n : G, N n -> f n = mon_unit) : QuotientGroup $-> A. Proof. snrapply Build_GroupHomomorphism. - srapply Quotient_rec. + exact f. + cbn; intros x y n. apply grp_moveR_M1. rhs_V nrapply (ap (.* f y) (grp_homo_inv _ _)). rhs_V nrapply grp_homo_op. symmetry; apply h; assumption. - intro x. refine (Quotient_ind_hprop _ _ _). intro y. revert x. refine (Quotient_ind_hprop _ _ _). intro x; simpl. apply grp_homo_op. Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Congruence. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import HSet. Require Import Spaces.Finite.Finite. Require Import WildCat. Require Import Modalities.Modality.