(X : Type) (P : Localize f X -> Type) (Ploc : forall i, ooExtendableAlong_Over (f i) (fun _ => Localize f X) (fun _ => P) (islocal_localize f X i)) : ooExtendableAlong loc P. Proof. intros n; generalize dependent P. simple_induction n n IHn; intros P Ploc. 1:exact tt. split. - intros g. exists (Localize_ind f X P g Ploc). intros x; reflexivity. - intros h k; apply IHn; intros i m. apply ooextendable_over_homotopy. exact (Ploc i). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.