{-# OPTIONS --safe #-}

open import Level

module Data.Empty.UniversePolymorphic {ℓ : Level} where

data ⊥ : Type ℓ where

absurd : ⊥ → A
absurd ()