abses_pullback_component1_id' {A B B' : AbGroup@{u}} {E : AbSES B A} {F : AbSES B' A} (f : AbSESMorphism E F) (h : component1 f == grp_homo_id) : E $== abses_pullback (component3 f) F. Proof. pose (g := abses_pullback_morphism_corec f). nrapply abses_path_data_to_iso. exists (component2 g); split. - exact (fun a => (left_square g a)^ @ ap _ (h a)). - reflexivity. Defined.
Require Import Basics Types. Require Import HSet Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Modalities.ReflectiveSubuniverse. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.