`{Funext} {B A : AbGroup@{u}} (E F: AbSES B A) : abses_path_data E F <~> abses_path_data_iso E F. Proof. srapply equiv_adjointify. - apply abses_path_data_to_iso. - srapply (functor_sigma (grp_iso_homo _ _)). exact (fun _ => idmap). - intros [phi [p q]]. apply path_sigma_hprop. by apply 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.