proposition: Proposition equiv_isoprojective_hasochoice `{Funext} (O : Modality) (X : Type) `{In O X} : IsOProjective O X <~> HasOChoice O X.
proof: Proof. refine (equiv_iff_hprop_uncurried (iff_isoprojective_hasochoice O X)). apply istrunc_forall. Defined.
imports: Basics Types Truncations.Core Truncations.SeparatedTrunc Modalities.Modality Modalities.Identity Limits.Pullback