Subuniverse. Proof. unshelve econstructor. - intros X; exact (In L X * In O X). - intros ? X; exact _. - intros T U [? ?] f feq; split; apply (inO_equiv_inO _ f). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.