abses_pullback_compose' {A B0 B1 B2 : AbGroup@{u}} (f : B0 $-> B1) (g : B1 $-> B2) : abses_pullback (A:=A) f o abses_pullback g $=> abses_pullback (g $o f). Proof. intro E; srefine (_; (_,_)). - apply equiv_grp_pullback_compose_r. - intro a. by srapply equiv_path_pullback_hset. - reflexivity. Defined.
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.