abses_pullback_const' {A B B' : AbGroup} : const pt $=> (@abses_pullback A B B' grp_homo_const). 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.
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.