proposition: Proposition hasochoice_oprojective (O : Modality) (X : Type) `{In O X} : IsOProjective O X -> HasOChoice O X.
proof: Proof. refine (_ o fst (iff_isoprojective_surjections_split O X)). intros splits P oP S. specialize splits with {x : X & P x} pr1. pose proof (splits _ (fst (iff_merely_issurjection P) S)) as M. clear S splits. strip_truncations; apply tr. destruct M as [s p]. intro x. exact (transport _ (p x) (s x).2). Defined.
imports: Basics Types Truncations.Core Truncations.SeparatedTrunc Modalities.Modality Modalities.Identity Limits.Pullback