{- Unit type. -} module basic.unit where open import basic.prelude record 𝟙 : Type where instance constructor tt