`{Univalence} {B A : AbGroup@{u}} {E F : AbSES' B A} : abses_path_data_iso E F <~> E = F. Proof. refine (_ oE shuffle_abses_path_data_iso E F). refine (equiv_ap_inv issig_abses _ _ oE _). refine (equiv_path_sigma_hprop _ _ oE _). refine (equiv_path_sigma _ _ _ oE _). srapply equiv_functor_sigma'. 1: exact equiv_path_abgroup. intro q; lazy beta. snrefine (equiv_concat_l _ _ oE _). 1: exact (q $o inclusion _, projection _ $o grp_iso_inverse q). 2: { refine (equiv_path_prod _ _ oE _). exact (equiv_functor_prod' equiv_path_grouphomomorphism equiv_path_grouphomomorphism). } refine (transport_prod _ _ @ _). apply path_prod'. - apply transport_iso_abgrouphomomorphism_from_const. - apply transport_iso_abgrouphomomorphism_to_const. 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.