proposition: Proposition iff_isabprojective_surjections_split (P : AbGroup) : IsAbProjective P <-> (forall A, forall p : A $-> P, IsSurjection p -> merely (exists s : P $-> A, p $o s == grp_homo_id)).
proof: Proof. split. - intros H A B. apply H. - intros H A B e f H1. pose proof (s := H (ab_pullback f e) (grp_pullback_pr1 f e) (conn_map_pullback _ f e)). strip_truncations. destruct s as [s h]. refine (tr ((grp_pullback_pr2 f e) $o s; _)); intro x. refine ((pullback_commsq f e _)^ @ _). exact (ap f (h x)). Defined.
imports: Basics Types AbelianGroup AbPullback WildCat.Core Limits.Pullback ReflectiveSubuniverse Truncations.Core