{A B : AbGroup} (E : AbSES' B A) : IsComplex (inclusion E) (projection E) := cx_isexact. Global Instance ispointed_abses {B A : AbGroup@{u}} : IsPointed (AbSES' B A). Proof. rapply (Build_AbSES (ab_biprod A B) ab_biprod_inl ab_biprod_pr2). snrapply Build_IsExact. - srapply phomotopy_homotopy_hset; reflexivity. - intros [[a b] p]; cbn; cbn in p. rapply contr_inhabited_hprop. apply tr. exists a. rapply path_sigma_hprop; cbn. exact (path_prod' idpath p^). Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.