fact: Definition O_lex_leq_eq {O1 O2 O3 : ReflectiveSubuniverse} `{O1 <=> O2} `{O2 << O3, O2 <<< O3} (Hstrong := O_strong_leq_trans_l O1 O2 O3) : O1 <<< O3.
imports: HoTT.Basics HoTT.Types HFiber Extensions Limits.Pullback Modality Accessible Localization