proposition: Proposition abext_projective_trivial `{Univalence} (P : AbGroup) (ext_triv : forall A, forall E : AbSES P A, tr E = point (Ext P A)) : IsAbProjective P.
proof: Proof. apply iff_isabprojective_surjections_split. intros E p issurj_p. apply (iff_ab_ext_trivial_split (abses_from_surjection p))^-1. apply ext_triv. Defined.
imports: Basics Types Truncations.Core Pointed WildCat Truncations.SeparatedTrunc AbelianGroup AbHom AbProjective AbSES.Pullback AbSES.BaerSum AbSES.Core