abses_pushout_component3_id' `{Univalence} {A A' B : AbGroup} {E : AbSES B A'} {F : AbSES B A} (f : AbSESMorphism E F) (h : component3 f == grp_homo_id) : abses_pushout (component1 f) E $== F. Proof. pose (g := abses_pushout_morphism_rec f). nrapply abses_path_data_to_iso. exists (component2 g); split. + intro x. exact (left_square g _)^. + intro x. exact ((right_square g _) @ h _)^. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat Pointed.Core Homotopy.ExactSequence HIT.epi. Require Import Modalities.ReflectiveSubuniverse. Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.