fact: Definition Cl' (U : HProp) : Modality := Nul (Build_NullGenerators U (fun _ => Empty)).
imports: HoTT.Basics HoTT.Types Extensions Modality Accessible Nullification Lex Topological Colimits.Pushout Homotopy.Join.Core