proposition: Proposition equiv_path_abses_iso `{Univalence} {B A : AbGroup@{u}} {E F : AbSES' B A} : abses_path_data_iso E F <~> E = F.
proof: 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.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse