(O : Modality) (X : Type) `{In O X} : IsOProjective O X -> HasOChoice O X. 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.
Require Import Basics Types. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Modalities.Modality Modalities.Identity. Require Import Limits.Pullback.