abses_pullback_point' {A B B' : AbGroup} (f : B' $-> B) : (abses_pullback f pt) $== (point (AbSES B' A)). Proof. snrefine (_; (_, _)). - snrapply Build_GroupIsomorphism. + srapply ab_biprod_corec. * refine (ab_biprod_pr1 $o _). apply grp_pullback_pr1. * apply projection. + srapply isequiv_adjointify. * snrapply grp_pullback_corec. -- exact (functor_ab_biprod grp_homo_id f). -- exact ab_biprod_pr2. -- reflexivity. * reflexivity. * intros [[a b] [b' c]]. srapply equiv_path_pullback_hset; split; cbn. 2: reflexivity. exact (path_prod' idpath c^). - reflexivity. - 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.