`{Univalence} {A B B' C D D' : AbGroup@{u}} {E : AbSES B A} {F : AbSES D C} (f : B' $-> B) (g : D' $-> D) : abses_pullback (functor_ab_biprod f g) (abses_direct_sum E F) = abses_direct_sum (abses_pullback f E) (abses_pullback g F) := (abses_pullback_component1_id (abses_directsum_pullback_morphism f g) (fun _ => idpath))^.
Require Import Basics Types. Require Import HSet Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Modalities.ReflectiveSubuniverse. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.