`{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. Proof. exists (abses_pullback_trivial_preimage E F p). srefine (_^$; _). 1: by rapply (abses_pullback_component1_id' (abses_pullback_inclusion0_map' E F p)). lazy beta; unfold pr2. refine (cat_assoc _ _ _ $@ _). refine (cat_assoc _ _ _ $@ _). apply gpd_moveR_Vh. apply gpd_moveL_hM. apply equiv_ab_biprod_ind_homotopy. split; apply equiv_path_pullback_rec_hset; split; cbn. - intro a. exact (ap (class_of _ o pullback_pr1) (fst p^$.2 a)). - intro a. exact ((snd p^$.2 _)^). - intro b; apply qglue. exists (-b). apply grp_moveL_Vg. refine ((grp_homo_op (grp_pullback_pr1 _ _ $o p^$.1 $o ab_biprod_inr) _ _)^ @ _). exact (ap _ (right_inverse _) @ grp_homo_unit _ @ (grp_homo_unit _)^). - intro b. exact (snd p^$.2 _)^. 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.