proposition: Theorem homotopic_isabelianization {G : Group} (A B : AbGroup) (eta1 : GroupHomomorphism G A) (eta2 : GroupHomomorphism G B) {isab1 : IsAbelianization A eta1} {isab2 : IsAbelianization B eta2} : eta2 == grp_homo_compose (groupiso_isabelianization A B eta1 eta2) eta1.
proof: Proof. intros x. exact (((esssurj (group_precomp B eta1) eta2).2 x)^). Defined.
imports: Basics Types Truncations.Core Cubical WildCat Colimits.Coeq Algebra.Groups.Group Algebra.AbGroups.AbelianGroup Modalities.ReflectiveSubuniverse