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