abses_pullback_pcompose' {B0 B1 B2 A : AbGroup} (f : B0 $-> B1) (g : B1 $-> B2) : abses_pullback' f $o* abses_pullback' g $=>* abses_pullback' (A:=A) (g $o f). Proof. exists (abses_pullback_compose' f g). intros [[[a b2] [b1 c]] [b0 c']]; cbn in c, c'. srapply equiv_path_pullback_hset; split; cbn. 2: reflexivity. exact (path_prod' idpath (c @ ap g c')). 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.