(O1 O2 : Subuniverse) `{O1 <=> O2} (A : Type) `{Reflects O1 A} : @Reflects O2 A (prereflects_O_leq O1 O2 A). Proof. constructor; intros B B_inO2. pose proof (inO_leq O2 O1 _ B_inO2). apply (extendable_to_O O1). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.