`{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) : abses_pullback_trivial_preimage E F p $== Y.1. Proof. destruct Y as [Y Q]. apply abses_path_data_to_iso; srefine (_; (_,_)). - snrapply (ab_cokernel_embedding_rec _ (grp_pullback_pr1 _ _$o (Q.1^$).1)). 1-3: exact _. intro f. nrefine (ap _ (induced_map_eq E F p (Y;Q) _) @ _); cbn. exact (grp_unit_r _ @ grp_homo_unit _). - intro a. refine (_ @ ap (grp_pullback_pr1 _ _) (fst (Q.1^$).2 a)). exact (grp_quotient_rec_beta' _ F _ _ (inclusion F a)). - nrapply (conn_map_elim _ grp_quotient_map). 1: apply issurj_class_of. 1: intros ?; apply istrunc_paths; apply group_isgroup. intro f. refine (ap (projection E) (snd (Q.1^$).2 f) @ _); unfold pr1. exact (pullback_commsq _ _ ((Q.1^$).1 f))^. 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.