{O' : Subuniverse} (O : ReflectiveSubuniverse) {A : Type} `{Reflects O' A} (inO_sigma : forall (B: O_reflector O' A -> Type), (forall oa, In O (B oa)) -> In O' {z:O_reflector O' A & B z}) : ReflectsD O' O A. Proof. constructor; intros B B_inO. intros n; generalize dependent A. induction n as [|n IHn]; intros; [ exact tt | cbn ]. refine (extension_from_inO_sigma O B , _). intros h k; rapply IHn. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.