{A B : Type} (C : B -> Type) (f : A -> B) (ext : ooExtendableAlong f C) (D : forall b, C b -> Type) (r s : forall b c, D b c) : ooExtendableAlong_Over f C D ext -> ooExtendableAlong_Over f C (fun b c => r b c = s b c) ext. Proof. intros ext' n. revert C ext D r s ext'. simple_induction n n IHn; intros C ext D r s ext'. 1:exact tt. split. - intros g g'. simple refine (_;_); simpl. + intros b. refine (_ @ (fst (snd (ext' 2) _ _ (fun b' => r b' ((fst (ext n.+1) g).1 b')) (fun b' => s b' ((fst (ext n.+1) g).1 b'))) (fun _ => 1) _).1 b). * refine (transport2 (D b) (p := 1) _ _). refine ((fst (snd (snd (ext 3) _ _) (fun b' => 1) ((fst (snd (ext 2) _ _) (fun a : A => 1)).1) ) _).1 b); intros a. symmetry; refine ((fst (snd (ext 2) _ _) (fun a' => 1)).2 a). * intros a; simpl. refine (_ @ ap (transport (D (f a)) ((fst (ext n.+1) g).2 a)^) (g' a) @ _); [ symmetry; by apply apD | by apply apD ]. + intros a; simpl. set (h := (fst (ext n.+1) g).1). match goal with |- context[ (fst (snd (ext' 2) _ _ ?k1 ?k2) (fun _ => 1) ?l).1 ] => pose (p := (fst (snd (ext' 2) _ _ k1 k2) (fun _ => 1) l).2 a); simpl in p end. rewrite transport_paths_Fl in p. apply moveL_Mp in p. refine (ap (transport _ _) (1 @@ p) @ _); clear p. unfold transport2; rewrite concat_p_pp. match goal with |- transport ?P ?p ((ap ?f ?q @ ap ?f ?r) @ ?s) = ?t => refine (ap (transport P p) ((ap_pp f q r)^ @@ (idpath s)) @ _) end. pose (p := (fst (snd (snd (ext 3) h h) (fun b' : B => 1) ((fst (snd (ext 2) h h) (fun a0 : A => 1)).1)) (fun a' : A => ((fst (snd (ext 2) h h) (fun a' : A => 1)).2 a')^)).2 a); simpl in p. refine (ap (transport _ _) (ap (ap _) (p @@ 1) @@ 1) @ _); clear p. rewrite concat_Vp; simpl; rewrite concat_1p. refine (transport_paths_FlFr_D _ _ @ _). Open Scope long_path_scope. rewrite !ap_pp, !concat_p_pp, ap_transport_pV. Local Opaque transport_pV. rewrite !concat_p_pp. Local Transparent transport_pV. refine ((((_ @@ 1) @ concat_1p _) @@ 1 @@ 1 @@ 1) @ _). * rewrite ap_V, concat_pp_p. do 2 apply moveR_Vp. rewrite concat_p1. symmetry; apply transport_pV_ap. * rewrite !concat_pp_p. refine ((1 @@ _) @ (concat_p1 _)). apply moveR_Vp; rewrite concat_p1. apply transport_pV_ap. Close Scope long_path_scope. - intros h k h' k'. refine (extendable_over_postcompose' _ _ _ _ _ _ (fun b c => equiv_cancelL (apD (r b) c) _ _) _). refine (IHn _ _ _ _ _ (fun n => snd (ext' n.+1) h k (fun b => r b (h b)) (fun b => s b (k b)))). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.