------------------------------------------------------------------------ -- Empty type (in Set1) ------------------------------------------------------------------------ module Data.Empty1 where data ⊥₁ : Set1 where