{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. 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.
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.