NullGenerators@{a1} -> LocalGenerators@{a2} := fun S => Build_LocalGenerators (ngen_indices S) (ngen_type S) (fun _ => Unit) (fun _ _ => tt).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions NullHomotopy. Require Import Modality. Module Import IsLocal_Internal. Module Import IsNull_Internal.