proposition: Proposition iff_ab_ext_trivial_split `{Univalence} {B A : AbGroup} (E : AbSES B A) : merely {s : GroupHomomorphism B E & (projection _) $o s == idmap} <~> (tr E = point (Ext B A)).
proof: Proof. refine (equiv_path_Tr _ _ oE _). srapply equiv_iff_hprop; apply Trunc_functor; apply iff_abses_trivial_split. Defined.
imports: Basics Types Truncations.Core Pointed WildCat Truncations.SeparatedTrunc AbelianGroup AbHom AbProjective AbSES.Pullback AbSES.BaerSum AbSES.Core