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