(n : nat) {A B : Type} (C : B -> Type) (f : A -> B) (ext : ExtendableAlong n f C) (D : B -> Type) : ExtendableAlong n f D -> ExtendableAlong_Over n f C (fun b _ => D b) ext. Proof. revert C ext D. simple_induction n n IHn; intros C ext D ext'. 1:exact tt. split. - intros g g'. exists ((fst ext' g').1). exact (fun a => transport_const ((fst ext g).2 a) _ @ (fst ext' g').2 a). - intros h k h' k'. refine (extendable_over_postcompose' _ _ _ _ _ _ _ (IHn (fun b => h b = k b) (snd ext h k) (fun b => h' b = k' b) (snd ext' h' k'))). exact (fun b c => equiv_concat_l (transport_const c (h' b)) (k' b)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.