abses_pushout_point' `{Univalence} {A A' B : AbGroup} (f : A $-> A') : abses_pushout f (point (AbSES B A)) $== pt. Proof. srapply abses_path_data_to_iso; srefine (_; (_,_)). - snrefine (ab_pushout_rec ab_biprod_inl _ _). + exact (functor_ab_biprod f grp_homo_id). + reflexivity. - intro a'. apply path_prod. + simpl. exact (ap _ (grp_homo_unit f) @ right_identity _). + simpl. exact (right_identity _). - srapply Quotient_ind_hprop. reflexivity. 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.