`{Univalence} {B A : AbGroup@{u}} {E F G : AbSES B A} (p : E = F) (q : F = G) : p @ q = equiv_path_abses_iso (abses_path_data_compose (equiv_path_abses_iso^-1 p) (equiv_path_abses_iso^-1 q)). Proof. induction p, q. refine (equiv_path_abses_1^ @ _). apply (ap equiv_path_abses_iso). apply path_sigma_hprop. by 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.