proposition: Lemma hfiber_cxfib'_induced_path' `{Univalence} {A B C : AbGroup} (E : AbSES C B) (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) (Y : hfiber_cxfib' E F p) : path_hfiber_cxfib' (hfiber_cxfib'_inhabited E F p) Y.
proof: Proof. exists (hfiber_cxfib'_induced_path'0 E F p Y). rapply gpd_moveR_Vh. rapply gpd_moveL_hM. rapply gpd_moveR_Vh. intro x. srapply equiv_path_pullback_hset; split. 2: exact (snd Y.2.1^$.2 x)^. reflexivity. Defined.
imports: Basics Types HSet HFiber Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.Pullback Modalities.Identity Modalities.Modality Truncations.Core