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

{-# OPTIONS --universe-polymorphism #-}

module Data.Empty where

open import Level

data ⊥ : Set where

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()