ooextendable_over_unit@{i j k l m} (A : Type@{i}) (C : Unit -> Type@{j}) (D : forall u, C u -> Type@{k}) (ext : ooExtendableAlong@{l l j m} (const_tt A) C) (ext' : forall (c : forall u, C u), ooExtendableAlong (const_tt A) (fun u => (D u (c u)))) : ooExtendableAlong_Over (const_tt A) C D ext := fun n => extendable_over_unit n A C D (ext n) (fun c => ext' c n).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import Modality Accessible.