`{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. 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.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.