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