grp_quotient_rec_beta' {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 := fun _ => idpath.
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.