`{Funext} {G : Group} {G_ab : AbGroup} (eta : GroupHomomorphism G G_ab) `{!IsAbelianization G_ab eta} (A : AbGroup) : IsEquiv (group_precomp A eta). Proof. snrapply isequiv_adjointify. - intros g. rapply (surjinj_inv (group_precomp A eta) g). - intros f. snrapply equiv_path_grouphomomorphism. exact (eisretr0gpd_inv (group_precomp A eta) f). - intros f. snrapply equiv_path_grouphomomorphism. exact (eissect0gpd_inv (group_precomp A eta) f). 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.