`{Univalence} {B A : AbGroup@{u}} {E : AbSES B A} : equiv_path_abses_iso (abses_path_data_1 E) = idpath. Proof. apply (equiv_ap_inv' equiv_path_abses_iso). refine (eissect _ _ @ _). srapply path_sigma_hprop; simpl. srapply equiv_path_groupisomorphism. reflexivity. Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.