{A B : Type} (C : B -> Type) (f : A -> B) (ext : ooExtendableAlong f C) (D : B -> Type) : ooExtendableAlong f D -> ooExtendableAlong_Over f C (fun b _ => D b) ext := fun ext' n => extendable_over_const n C f (ext n) D (ext' n).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.