{O1 O2 O3 : ReflectiveSubuniverse} `{O1 <=> O2} `{O2 << O3, O2 <<< O3} (Hstrong := O_strong_leq_trans_l O1 O2 O3) : O1 <<< O3. Proof. intros A; unshelve econstructor; intros P P_inO1. all:pose (P_inO2 := fun x => inO_leq O1 O2 _ (P_inO1 x)). - apply (OO_descend O3 O2 P). - intros x; apply (inO_leq O2 O1), (OO_descend_inO O3 O2 P). - apply (OO_descend_beta O3 O2 P). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.