fact: Definition abses_pushout_path_data_1 `{Univalence} {A A' B : AbGroup} (f : A $-> A') {E : AbSES B A} : fmap (abses_pushout f) (Id E) = Id (abses_pushout f E).
imports: Basics Types Truncations.Core WildCat Pointed.Core Homotopy.ExactSequence HIT.epi Modalities.ReflectiveSubuniverse AbelianGroup AbPushout AbHom AbGroups.Biproduct AbSES.Core AbSES.DirectSum