equiv_path_hfiber_cxfib' `{Univalence} {A B C : AbGroup} {E : AbSES C B} (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) (U V : hfiber_cxfib' E F p) : path_hfiber_cxfib' U V <~> U = V. Proof. refine (equiv_path_sigma _ _ _ oE _). srapply (equiv_functor_sigma' equiv_path_abses_iso); intro q; lazy beta. refine (equiv_path_sigma_hprop _ _ oE _). refine (equiv_concat_l _ _ oE _). 1: apply transport_hfiber_abses_path_cxfib'_l. refine (equiv_path_sigma_hprop _ _ oE equiv_concat_l _ _ oE _). 1: { refine (ap (fun x => (fmap (abses_pullback _) x $@ _).1) _). nrefine (ap _ (abses_path_data_V q) @ _). apply eissect. } refine (equiv_concat_l _ _ oE _). 1: { refine (ap (fun x => (x $@ _).1) _). rapply gpd_strong_1functor_V. } apply equiv_path_groupisomorphism. Defined.
Require Import Basics Types HSet HFiber Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Groups.QuotientGroup. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.Pullback. Require Import Modalities.Identity Modalities.Modality Truncations.Core.