(n : nat) (A : Type@{a}) (C : Unit -> Type@{i}) (D : forall u, C u -> Type@{j}) (ext : ExtendableAlong@{a a i k} n (const_tt A) C) (ext' : forall (c : forall u, C u), ExtendableAlong@{a a j k} n (const_tt A) (fun u => (D u (c u)))) : ExtendableAlong_Over@{a a i j k} n (const_tt A) C D ext. Proof. generalize dependent C; simple_induction n n IH; intros C D ext ext'; [exact tt | split]. - intros g g'. exists ((fst (ext' (fst ext g).1) (fun a => ((fst ext g).2 a)^ # (g' a))).1); intros a; simpl. apply moveR_transport_p. exact ((fst (ext' (fst ext g).1) (fun a => ((fst ext g).2 a)^ # (g' a))).2 a). - intros h k h' k'. apply IH; intros g. exact (snd (ext' k) (fun u => g u # h' u) k'). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import Modality Accessible.