ooExtendableAlong_Over@{a b c d m | a <= m, b <= m, c <= m, d <= m} {A : Type@{a}} {B : Type@{b}} (f : A -> B) (C : B -> Type@{c}) (D : forall b, C b -> Type@{d}) (ext : ooExtendableAlong f C) := forall n, ExtendableAlong_Over@{a b c d m} n f C D (ext n).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.