fact: Definition ooextendable_TypeO_lex_leq `{Univalence} {A B : Type} (f : A -> B) `{O_inverts O' f} : ooExtendableAlong f (fun _ => Type_ O).
imports: HoTT.Basics HoTT.Types HFiber Extensions Limits.Pullback Modality Accessible Localization