`{Univalence} {A B B' : AbGroup} {f : B' $-> B} (Y : AbSES B' A) (U V : graph_hfiber (abses_pullback f) Y) : hfiber_abses_path U V <~> U = V. Proof. refine (equiv_path_sigma _ _ _ oE _). srapply (equiv_functor_sigma' equiv_path_abses_iso); intro p; lazy beta. refine (equiv_concat_l _ _ oE _). { refine (transport_path_data_hfiber_abses_pullback_l _ @ _). refine (ap (fun x => (fmap (abses_pullback f) x) $@ _) _ @ _). { refine (ap _ (abses_path_data_V p) @ _). apply eissect. } refine (ap (fun x => x $@ _) _). rapply gpd_strong_1functor_V. } refine (equiv_path_sigma_hprop _ _ oE _). apply equiv_path_groupisomorphism. 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.