{F : Funext} {G : AbGroup} (N : Subgroup G) (H : Group) : {f : GroupHomomorphism G H & forall (n : G), N n -> f n = mon_unit} <~> (GroupHomomorphism (QuotientAbGroup G N) H). Proof. exact (equiv_grp_quotient_ump (Build_NormalSubgroup G N _) _). Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.