fact: Definition abses_path_pushout_inclusion_commsq `{Univalence} {A A' B : AbGroup} (alpha : A $-> A') (E : AbSES B A) (F : AbSES B A') (p : abses_pushout alpha E = F) : exists phi : middle E $-> F, inclusion F o alpha == phi o inclusion E.
imports: Basics Types Truncations.Core WildCat Pointed.Core Homotopy.ExactSequence HIT.epi Modalities.ReflectiveSubuniverse AbelianGroup AbPushout AbHom AbGroups.Biproduct AbSES.Core AbSES.DirectSum