(O : Modality@{i}) : ReflectiveSubuniverse@{i}. Proof. refine (Build_ReflectiveSubuniverse (modality_subuniv O) (modality_prereflects O) _). intros T; constructor. intros Q Q_inO. srapply extendable_to_OO. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.