proposition: Lemma abses_ap_fmap `{Univalence} {B0 B1 A0 A1 : AbGroup@{u}} (f : AbSES B0 A0 -> AbSES B1 A1) `{!Is0Functor f, !Is1Functor f} {E F : AbSES B0 A0} (p : E $== F) : ap f (equiv_path_abses_iso p) = equiv_path_abses_iso (fmap f p).
proof: Proof. revert p. apply (equiv_ind equiv_path_abses_iso^-1%equiv); intro p. induction p. refine (ap (ap f) (eisretr _ _) @ _). nrefine (_ @ ap equiv_path_abses_iso _). 2: { rapply path_hom. srefine (_ $@ fmap2 _ _). 2: exact (Id E). 2: intro x; reflexivity. exact (fmap_id f _)^$. } exact equiv_path_abses_1^. Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse