`{Univalence} {B A : AbGroup@{u}} {E F G : AbSES B A} (p : abses_path_data_iso E F) (q : abses_path_data_iso F G) : equiv_path_abses_iso p @ equiv_path_abses_iso q = equiv_path_abses_iso (abses_path_data_compose p q). Proof. generalize p, q. equiv_intro ((equiv_path_abses_iso (E:=E) (F:=F))^-1) x. equiv_intro ((equiv_path_abses_iso (E:=F) (F:=G))^-1) y. refine ((eisretr _ _ @@ eisretr _ _) @ _). rapply abses_path_compose_beta. 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.