cxfib' {A B C : AbGroup} (E : AbSES C B) : AbSES C A -> graph_hfiber (abses_pullback (A:=A) (inclusion E)) pt. Proof. intro Y. exists (abses_pullback (projection E) Y). refine (abses_pullback_compose' _ _ Y $@ _). refine (abses_pullback_homotopic' _ grp_homo_const _ Y $@ _). 1: rapply iscomplex_abses. symmetry; apply abses_pullback_const'. Defined.
Require Import Basics Types HSet HFiber Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Groups.QuotientGroup. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.Pullback. Require Import Modalities.Identity Modalities.Modality Truncations.Core.