`{Univalence} {A B : AbGroup} (E : AbSES B A) : abses_baer_sum E (point (AbSES B A)) = E. Proof. refine (ap (abses_baer_sum E) _ @ _). - exact (abses_pullback_const E). - refine (ap (fun F => abses_baer_sum F (abses_pullback grp_homo_const E)) (abses_pullback_id E)^ @ _). refine ((baer_sum_distributive_pullbacks grp_homo_id grp_homo_const)^ @ _). refine (ap (fun f => abses_pullback f E) (grp_unit_r (G := ab_hom _ _) _) @ _). apply abses_pullback_id. Defined.
Require Import Basics Types. Require Import WildCat Pointed.Core. Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom. Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum. Require Import Homotopy.HSpace.Core.