(P : AbGroup) : IsAbProjective P <-> (forall A, forall p : A $-> P, IsSurjection p -> merely (exists s : P $-> A, p $o s == grp_homo_id)). 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.
Require Import Basics Types AbelianGroup AbPullback