`{Univalence} {A B : AbGroup} : abses_pullback (A:=A) (@grp_homo_id B) == idmap. Proof. intro E. apply equiv_path_abses_iso; srefine (_; (_, _)). 1: rapply (Build_GroupIsomorphism _ _ (grp_pullback_pr1 _ _)). 1: reflexivity. intros [a [p q]]; cbn. exact q^. 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.