equiv_hfiber_cxfib' `{Univalence} {A B C : AbGroup} {E : AbSES C B} (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) : hfiber_cxfib' E F p <~> hfiber (cxfib (iscomplex_pullback_abses E)) (equiv_hfiber_abses _ pt (F;p)). Proof. srapply equiv_functor_sigma_id; intro U; lazy beta. refine (_ oE equiv_hfiber_abses_pullback _ _ _). refine (_ oE equiv_ap' (equiv_hfiber_abses _ pt) _ _). apply equiv_concat_l. apply eq_cxfib_cxfib'. 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.