`{Univalence} (A B X Y : AbGroup) (E : AbSES B A) (F : AbSES Y X) (f : AbSESMorphism E F) : f = absesmorphism_compose (abses_pushout_morphism_rec f) (abses_pushout_morphism E (component1 f)). Proof. apply (equiv_ap issig_AbSESMorphism^-1 _ _). srapply path_sigma_hprop. 1: apply path_prod. 1: apply path_prod. all: apply equiv_path_grouphomomorphism; intro x; simpl. 1,3: reflexivity. rewrite grp_homo_unit. exact (left_identity _)^. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat Pointed.Core Homotopy.ExactSequence HIT.epi. Require Import Modalities.ReflectiveSubuniverse. Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.