fact: Definition null_to_local_generators : NullGenerators@{a1} -> LocalGenerators@{a2} := fun S => Build_LocalGenerators (ngen_indices S) (ngen_type S) (fun _ => Unit) (fun _ _ => tt).
imports: HoTT.Basics HoTT.Types Extensions NullHomotopy Modality