(S : NullGenerators@{a}) (X : Type@{i}) := IsLocal@{i i a} (null_to_local_generators@{a a} S) X.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions NullHomotopy. Require Import Modality. Module Import IsLocal_Internal. Module Import IsNull_Internal.