`{Univalence} {A A' B : AbGroup} (f : A $-> A') {E : AbSES B A} : fmap (abses_pushout f) (Id E) = Id (abses_pushout f E). Proof. srapply path_sigma_hprop. apply equiv_path_groupisomorphism. srapply Quotient_ind_hprop. intros [a' e]; simpl. apply qglue. refine (tr (0; _)). apply path_prod'; cbn. - refine (ap _ (grp_homo_unit _) @ _). refine (negate_mon_unit @ _). apply grp_moveL_Vg. exact (right_identity _ @ right_identity _). - refine (grp_homo_unit _ @ _). apply grp_moveL_Vg. exact (right_identity _ @ left_identity _). 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.