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