`{Univalence} {A A' B B' : AbGroup} {E : AbSES B A} {E' : AbSES B' A'} (f : AbSESMorphism E E') : abses_pushout (component1 f) E = abses_pullback (component3 f) E' := equiv_path_abses_iso (' f).
Require Import Basics Types. Require Import WildCat Pointed.Core. Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom. Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum. Require Import Homotopy.HSpace.Core.