`{Univalence} (P : AbGroup) (ext_triv : forall A, forall E : AbSES P A, tr E = point (Ext P A)) : IsAbProjective P. 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.
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.