(O : ReflectiveSubuniverse) (H : forall (A:Type) (B:A -> Type) {A_inO : In O A} `{forall a, In O (B a)}, (In O {x:A & B x})) : Modality. Proof. refine (Build_Modality' O _ _). intros; srapply reflectsD_from_inO_sigma. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.