extendable_over_postcompose' (n : nat) {A B : Type} (C : B -> Type) (f : A -> B) (ext : ExtendableAlong n f C) (D E : forall b, C b -> Type) (g : forall b c, D b c <~> E b c) : ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext. Proof. revert C ext D E g; simple_induction n n IHn; intros C ext D E g; simpl. 1:by apply idmap. intros ext'. split. - intros h k. exists (fun b => g b ((fst ext h).1 b) ((fst ext' h (fun a => (g _ _)^-1 (k a))).1 b)). intros a. refine ((ap_transport ((fst ext h).2 a) (g (f a)) _)^ @ _). apply moveR_equiv_M. exact ((fst ext' h (fun a => (g _ _)^-1 (k a))).2 a). - intros p q p' q'. refine (IHn (fun b => p b = q b) _ (fun b => fun c => transport (D b) c ((g b (p b))^-1 (p' b)) = ((g b (q b))^-1 (q' b))) _ _ (snd ext' p q (fun b => (g b (p b))^-1 (p' b)) (fun b => (g b (q b))^-1 (q' b)))). intros b c. refine (_ oE equiv_moveR_equiv_M _ _). apply equiv_concat_l. refine (_ @ (ap_transport c (g b) _)^). apply ap, symmetry, eisretr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.