`{Univalence} {A B0 B1 B2 : AbGroup} (f : B0 $-> B1) (g : B1 $-> B2) (h : g $o f == grp_homo_const) : IsComplex (abses_pullback_pmap (A:=A) g) (abses_pullback_pmap f). Proof. refine (_ @* _). 2: symmetry; exact pmap_abses_const_to_pointed. refine (to_pointed_compose _ _ @* _). apply equiv_ptransformation_phomotopy. by rapply '. 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.