(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. 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.
Require Import Basics Types. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Modalities.Modality Modalities.Identity. Require Import Limits.Pullback.