`{Univalence} {A B : AbGroup} : abses_pullback_pmap (A:=A) (@grp_homo_id B) ==* pmap_idmap. Proof. srapply Build_pHomotopy. 1: apply abses_pullback_id. refine (_ @ (concat_p1 _)^). nrapply (ap equiv_path_abses_iso). apply path_sigma_hprop. apply equiv_path_groupisomorphism. intros [[a b] [b' p]]; cbn; cbn in p. by apply path_prod'. Defined.
Require Import Basics Types. Require Import HSet Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Modalities.ReflectiveSubuniverse. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.