`{Funext} (O : ReflectiveSubuniverse) {X : Type} `{Reflects (Sep O) X} (P : O_reflector (Sep O) X -> Type) `{forall x, In O (P x)} : IsEquiv (fun g : (forall y, P y) => g o to (Sep O) X) := isequiv_ooextendable _ _ (extendable_to_OO P).
Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath. Require Import HFiber Extensions Factorization Limits.Pullback. Require Import Modality Accessible Descent. Require Import Truncations.Core. Require Import Homotopy.Suspension.