`{Univalence} {A B B' : AbGroup} {f : B' $-> B} {Y : AbSES B' A} {X0 : graph_hfiber (abses_pullback f) Y} {X1 : AbSES B A} (p : X0.1 = X1) : transport (fun x : AbSES B A => abses_pullback f x $== Y) p X0.2 = fmap (abses_pullback f) (equiv_path_abses_iso^-1 p^) $@ X0.2. Proof. induction p. refine (transport_1 _ _ @ _). nrefine (_ @ (ap (fun x => x $@ _)) _). 2: { refine (_ @ ap _ equiv_path_absesV_1^). exact (fmap_id_strong _ _)^. } exact (cat_idr_strong _)^. 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.