{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. intros x. exact (((esssurj (group_precomp B eta1) eta2).2 x)^). 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.