proposition: Theorem equiv_grp_quotient_ump {F : Funext} {G : Group} (N : NormalSubgroup G) (H : Group) : {f : G $-> H & forall (n : G), N n -> f n = mon_unit} <~> (G / N $-> H).
proof: Proof. srapply equiv_adjointify. - intros [f p]. exact (grp_quotient_rec _ _ f p). - intro f. exists (f $o grp_quotient_map). intros n h; cbn. refine (_ @ grp_homo_unit f). apply ap. apply qglue; cbn. rewrite right_identity; by apply issubgroup_in_inv. - intros f. rapply equiv_path_grouphomomorphism. by srapply Quotient_ind_hprop. - intros [f p]. srapply path_sigma_hprop; simpl. exact (grp_quotient_rec_beta N H f p). 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