{G : Group} (A B : AbGroup) (eta1 : GroupHomomorphism G A) (eta2 : GroupHomomorphism G B) {isab1 : IsAbelianization A eta1} {isab2 : IsAbelianization B eta2} : A ≅ B. Proof. destruct (esssurj (group_precomp B eta1) eta2) as [a ac]. destruct (esssurj (group_precomp A eta2) eta1) as [b bc]. srapply (Build_GroupIsomorphism _ _ a). srapply (isequiv_adjointify _ b). { refine (essinj (group_precomp B eta2) (x := a $o b) (y := Id (A := Group) B) _). intros x; cbn in *. refine (_ @ ac x). apply ap, bc. } { refine (essinj (group_precomp A eta1) (x := b $o a) (y := Id (A := Group) A) _). intros x; cbn in *. refine (_ @ bc x). apply ap, ac. } Defined.
Require Import Basics Types Truncations.Core. Require Import Cubical.DPath WildCat. Require Import Colimits.Coeq. Require Import Algebra.AbGroups.AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.