Source code on Github
------------------------------------------------------------------------
-- The Agda standard library
--
-- Level polymorphic Empty type
------------------------------------------------------------------------

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

module Data.Empty.Polymorphic where

import Data.Empty as Empty
open import Level

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

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