proposition: Proposition iff_isoprojective_surjections_split (O : Modality) (X : Type) `{In O X} : IsOProjective O X <-> (forall (Y : Type), In O Y -> forall (p : Y -> X), IsSurjection p -> merely (exists s : X -> Y, p o s == idmap)).
proof: Proof. split. - intros isprojX Y oY p S; unfold IsOProjective in isprojX. exact (isprojX Y _ X _ idmap p S). - intro splits. unfold IsOProjective. intros A oA B oB f p S. pose proof (splits (Pullback p f) _ pullback_pr2 _) as s'. strip_truncations. destruct s' as [s E]. refine (tr (pullback_pr1 o s; _)). intro x. refine (pullback_commsq p f (s x) @ _). apply (ap f). apply E. Defined.
imports: Basics Types Truncations.Core Truncations.SeparatedTrunc Modalities.Modality Modalities.Identity Limits.Pullback