`{Univalence} {G : Group} (N : NormalSubgroup G) : GroupIsomorphism N (grp_kernel (@grp_quotient_map G N)). Proof. srapply Build_GroupIsomorphism. - srapply (grp_kernel_corec (subgroup_incl N)). intro x; cbn. apply qglue. apply issubgroup_in_op. + exact (issubgroup_in_inv _ x.2). + exact issubgroup_in_unit. - apply isequiv_surj_emb. 2: apply (cancelL_isembedding (g:=pr1)). intros [g p]. rapply contr_inhabited_hprop. srefine (tr ((g; _); _)). + rewrite <- grp_unit_l, <- negate_mon_unit. apply (related_quotient_paths (fun x y => N (-x * y))). exact p^. + srapply path_sigma_hprop. reflexivity. 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.