proposition: Lemma ap_abses_pullback_data `{Univalence} {A B B' : AbGroup} (f : B' $-> B) {E F : AbSES B A} (p : abses_path_data_iso E F) : ap (abses_pullback f) (equiv_path_abses_iso p) = equiv_path_abses_iso (fmap (abses_pullback f) p).
proof: Proof. refine (ap_abses_pullback _ _ @ _). apply (ap (equiv_path_abses_iso o _)). apply eissect. Defined.
imports: Basics Types HSet Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Modalities.ReflectiveSubuniverse AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.DirectSum