iscomplex_abses_pullback' {A B0 B1 B2 : AbGroup} (f : B0 $-> B1) (g : B1 $-> B2) (h : g $o f == grp_homo_const) : abses_pullback' f $o* abses_pullback' g $=>* @pmap_abses_const _ _ _ A. Proof. refine (abses_pullback_pcompose' _ _ $@* _). refine (abses_pullback_phomotopic' _ _ h $@* _). exact abses_pullback_pconst'^*$. 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.