{fs : Funext} (O' O : Subuniverse) {A : Type} `{ReflectsD O' O A} (B : O_reflector O' A -> Type) `{forall a, In O (B a)} : IsEquiv (fun (h : forall oa, B oa) => h oD to O' A). Proof. apply isequiv_ooextendable, extendable_to_OO; assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.