`{Univalence} {A A' B : AbGroup} (f : A $-> A') {E F : AbSES B A} (p : E = F) : ap (abses_pushout f) p = equiv_path_abses_iso (fmap (abses_pushout f) (equiv_path_abses_iso^-1 p)). Proof. induction p. refine (_ @ ap _ _). 2: refine ((abses_pushout_path_data_1 f)^ @ ap _ equiv_path_absesV_1^). exact equiv_path_abses_1^. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat Pointed.Core Homotopy.ExactSequence HIT.epi. Require Import Modalities.ReflectiveSubuniverse. Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.