Loc@{a i} (f : LocalGenerators@{a}) : ReflectiveSubuniverse@{i}. Proof. snrefine (Build_ReflectiveSubuniverse (Build_Subuniverse (IsLocal f) _ _) (fun A => Build_PreReflects _ A (Localize f A) _ (@loc f A)) (fun A => Build_Reflects _ _ _ _)). - intros ? T; unfold IsLocal. nrefine (istrunc_forall@{a i i}); try assumption. intros i. apply ishprop_ooextendable@{a a i i i i i i i i i i i i i i}. - apply islocal_equiv_islocal. - apply islocal_localize. - cbn. intros Q Q_inO. apply ext_localize_ind; intros ?. apply ooextendable_over_const. apply Q_inO. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.