(f : LocalGenerators@{a}) (X : Type@{i}) {Y : Type@{j}} (Xloc : IsLocal@{i i' a} f X) (g : X -> Y) `{IsEquiv@{i j} _ _ g} : IsLocal@{j j' a} f Y. Proof. intros i. apply lift_ooextendablealong@{a a a a a a j j j k j'}. refine (ooextendable_postcompose@{a a i j k k k k k k} _ _ (f i) (fun _ => g) _). apply lift_ooextendablealong@{a a a a a a i i i i' k}. apply Xloc. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.