Nul@{a i} (S : NullGenerators@{a}) : Modality@{i}. Proof. simple refine (Build_Modality' (Loc (null_to_local_generators S)) _ _). - exact _. - intros A. snrefine (reflectsD_from_OO_ind@{i} _ _ _). + intros B B_inO g. refine (Localize_ind@{a i i i} (null_to_local_generators S) A B g _); intros i. apply ooextendable_over_unit; intros c. refine (ooextendable_postcompose@{a a i i i i i i i i} (fun (_:Unit) => B (c tt)) _ _ (fun u => transport B (ap@{Set _} c (path_unit tt u))) _). refine (ooextendable_islocal _ i). + reflexivity. + apply inO_paths@{i i}. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import Modality Accessible.