    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Level polymorphic Empty type
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Empty.Polymorphic where

    import Data.Empty as Empty using (⊥; ⊥-elim)
    open import Level using (Level; Lift; _⊔_)

    ⊥ : {ℓ : Level} → Set ℓ
    ⊥ {ℓ} = Lift ℓ Empty.⊥

    -- make ⊥-elim dependent too, as it does seem useful
    ⊥-elim : ∀ {w ℓ} {Whatever : ⊥ {ℓ} → Set w} → (witness : ⊥ {ℓ}) → Whatever witness
    ⊥-elim ()