------------------------------------------------------------------------
-- Empty type
------------------------------------------------------------------------

module Data.Empty where

data ⊥ : Set where

⊥-elim : {whatever : Set} → ⊥ → whatever
⊥-elim ()