{X : Type@{i}} {Xloc : IsLocal f X} i : ooExtendableAlong@{a a i k} (f i) (fun _ => X) := (lift_ooextendablealong _ _ (Xloc i)).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.