(O1 O2 O3 : ReflectiveSubuniverse) `{O1 <= O2} `{O2 << O3} : O1 << O3. Proof. intros A; constructor; intros B B_inO. apply (extendable_to_OO (O := O2)). intros x. srapply inO_leq; apply B_inO. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.