`{Univalence} {B A : AbGroup@{u}} {E F : AbSES B A} (phi : GroupIsomorphism E F) (p : phi $o inclusion _ == inclusion _) (q : projection _ == projection _ $o phi) : E = F := equiv_path_abses_iso (phi; (p,q)).
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.