`{Univalence} {B A G : AbGroup@{u}} (E : AbSES B A) : GroupHomomorphism (ab_hom A G) (ab_ext B G). Proof. snrapply Build_GroupHomomorphism. 1: exact (fun f => fmap01 (A:=AbGroup^op) Ext' _ f (tr E)). intros f g; cbn. nrapply (ap tr). exact (baer_sum_distributive_pushouts f g). Defined.
Require Import Basics Types Truncations.Core. Require Import Pointed WildCat. Require Import Truncations.SeparatedTrunc. Require Import AbelianGroup AbHom AbProjective. Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.