`{Funext} (O : Modality) {A : Type} (B : O A -> Type) `{forall a, In O (B a)} : IsEquiv (fun (h : forall oa, B oa) => h oD to O A). Proof. srapply (isequiv_oD_to_O O O). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.