proposition: Lemma abses_pullback_const' {A B B' : AbGroup} : const pt $=> (@abses_pullback A B B' grp_homo_const).
proof: Proof. intro E. simpl. nrapply abses_path_data_to_iso. srefine (_;(_,_)); cbn. - srapply grp_pullback_corec. + exact (inclusion _ $o ab_biprod_pr1). + exact ab_biprod_pr2. + intro x; cbn. apply iscomplex_abses. - intro a; cbn. by srapply equiv_path_pullback_hset; split. - reflexivity. Defined.
imports: Basics Types HSet Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Modalities.ReflectiveSubuniverse AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.DirectSum