forall (f : LocalGenerators@{a}) (X : Type@{i}), IsLocal@{i k a} f (Localize f X).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.