fact: Definition isequiv_oD_to_O {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).
imports: HoTT.Basics HoTT.Types HFiber Extensions Factorization Limits.Pullback ReflectiveSubuniverse