fact: Definition abses_pushout_const `{Univalence} {B A A' : AbGroup} (E : AbSES B A) : abses_pushout grp_homo_const E = pt :> AbSES B A' := abses_pushout_component3_id (abses_pushout_const_morphism E) (fun _ => idpath).
imports: Basics Types Truncations.Core WildCat Pointed.Core Homotopy.ExactSequence HIT.epi Modalities.ReflectiveSubuniverse AbelianGroup AbPushout AbHom AbGroups.Biproduct AbSES.Core AbSES.DirectSum