proposition: Lemma baer_sum_unit_r `{Univalence} {A B : AbGroup} (E : AbSES B A) : abses_baer_sum E (point (AbSES B A)) = E.
proof: 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.
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core