proposition: Corollary equiv_isoprojective_surjections_split `{Funext} (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. exact (equiv_iff_hprop_uncurried (iff_isoprojective_surjections_split O X)). Defined.
imports: Basics Types Truncations.Core Truncations.SeparatedTrunc Modalities.Modality Modalities.Identity Limits.Pullback