------------------------------------------------------------------------ -- The unit type (in Set₁) ------------------------------------------------------------------------ module Data.Unit1 where record ⊤₁ : Set₁ where