    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Empty values (e.g. [] for List, nothing for Maybe)
    ------------------------------------------------------------------------

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

    module Effect.Empty where

    open import Level using (Level; suc; _⊔_)

    private
      variable
        ℓ ℓ′ : Level
        A  : Set ℓ

    record RawEmpty (F : Set ℓ → Set ℓ′) : Set (suc ℓ ⊔ ℓ′) where
      field
        empty : F A

      -- backwards compatibility: unicode variants
      ∅ : F A
      ∅ = empty