`{Funext} {G : Group} {G_ab : AbGroup} (eta : GroupHomomorphism G G_ab) `{!IsAbelianization G_ab eta} (A : AbGroup) : (G_ab $-> A) <~> (G $-> A) := Build_Equiv _ _ _ (isequiv_group_precomp_isabelianization eta A). Section Abel. Context (G : Group). Local uncurry2 {A B C D : Type} : (A -> B -> C -> D) -> A * B * C -> D. Proof. intros f [[a b] c]. by apply 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.