`{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) : hfiber_cxfib'_induced_map E F p Y == abses_pullback_splits_induced_map' E Y.1. Proof. intros [a b]; cbn. refine (ap pullback_pr1 (fmap_hfiber_abses_lemma _ _ (F;p) Y.2 _) @ _). srapply equiv_path_pullback_hset; split; cbn. - exact (grp_unit_r _)^. - exact (grp_unit_l _)^. 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.