proposition: Proposition iff_isoprojective_hasochoice (O : Modality) (X : Type) `{In O X} : IsOProjective O X <-> HasOChoice O X.
proof: Proof. split. - apply hasochoice_oprojective. exact _. - apply isoprojective_ochoice. Defined.
imports: Basics Types Truncations.Core Truncations.SeparatedTrunc Modalities.Modality Modalities.Identity Limits.Pullback