proposition: Proposition isoprojective_ochoice (O : Modality) (X : Type) : HasOChoice O X -> IsOProjective O X.
proof: Proof. intros chX A ? B ? f p S. assert (g : merely (forall x:X, hfiber p (f x))). - rapply chX. intro x. exact (center _). - strip_truncations; apply tr. exists (fun x:X => pr1 (g x)). intro x. exact (g x).2. Defined.
imports: Basics Types Truncations.Core Truncations.SeparatedTrunc Modalities.Modality Modalities.Identity Limits.Pullback