`{Univalence} {A B B' : AbGroup} (f : B' $-> B) {E F : AbSES B A} (p : E = F) : ap (abses_pullback f) p = equiv_path_abses_iso (fmap (abses_pullback f) (equiv_path_abses_iso^-1 p)). Proof. induction p. nrefine (_ @ ap equiv_path_abses_iso _). 2: refine ((fmap_id_strong _ _)^ @ ap _ equiv_path_absesV_1^). exact equiv_path_abses_1^. Defined.
Require Import Basics Types. Require Import HSet Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Modalities.ReflectiveSubuniverse. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.