{O' : Subuniverse} (O : ReflectiveSubuniverse) {A : Type} `{PreReflects O' A} `{IsConnMap O _ _ (to O' A)} : ReflectsD O' O A. Proof. constructor; rapply ooextendable_conn_map_inO. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.