{A B : AbGroup} (E : AbSES B A) : (B $-> A) -> abses_path_data E E. Proof. intro phi. srefine (_; (_, _)). - exact (ab_homo_add grp_homo_id (inclusion E $o phi $o projection E)). - intro a; cbn. refine (ap (fun x => _ + inclusion E (phi x)) _ @ _). 1: apply iscomplex_abses. refine (ap (fun x => _ + x) (grp_homo_unit (inclusion E $o phi)) @ _). apply grp_unit_r. - intro e; symmetry. refine (grp_homo_op (projection E) _ _ @ _); cbn. refine (ap (fun x => _ + x) _ @ _). 1: apply iscomplex_abses. apply grp_unit_r. 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.