`{Univalence} {B' A' B A : AbGroup@{u}} {f g : AbSES B A -->* AbSES B' A'} : f $=>* g <~> to_pointed f ==* to_pointed g. Proof. refine (issig_pforall _ _ oE _). apply (equiv_functor_sigma' (equiv_path_data_homotopy f g)); intro h. refine (equiv_concat_r _ _ oE _). 1: exact ((abses_path_data_compose_beta _ _)^ @ ap (fun x => _ @ x) (abses_path_data_V _)^). refine (equiv_ap' equiv_path_abses_iso _ _ oE _). refine (equiv_path_sigma_hprop _ _ oE _). apply equiv_path_groupisomorphism. 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.