`{Univalence} {B' A' B A : AbGroup@{u}} : (AbSES B A -->* AbSES B' A') -> (AbSES B A ->* AbSES B' A') := fun f => Build_pMap _ _ f (equiv_path_abses_iso (bp_pointed f)).
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.