proposition: Corollary grp_quotient_rec_beta `{F : Funext} {G : Group} (N : NormalSubgroup G) (H : Group) {A : Group} (f : G $-> A) (h : forall n:G, N n -> f n = mon_unit) : (grp_quotient_rec G N f h) $o grp_quotient_map = f.
proof: Proof. apply equiv_path_grouphomomorphism; reflexivity. Defined.
imports: Basics Types Truncations.Core Algebra.Congruence Algebra.Groups.Group Algebra.Groups.Subgroup Algebra.Groups.Image Algebra.Groups.Kernel Colimits.Quotient HSet Spaces.Finite.Finite WildCat Modalities.Modality