proposition: Proposition abext_trivial_projective `{Univalence} (P : AbGroup) `{IsAbProjective P} : forall A, forall E : AbSES P A, tr E = point (Ext P A).
proof: Proof. intros A E. apply iff_ab_ext_trivial_split. exact (fst (iff_isabprojective_surjections_split P) _ _ _ _). Defined.
imports: Basics Types Truncations.Core Pointed WildCat Truncations.SeparatedTrunc AbelianGroup AbHom AbProjective AbSES.Pullback AbSES.BaerSum AbSES.Core