{-# OPTIONS --safe --no-import-sorts #-}

open import Axiom.Set using (Theory)

module Class.HasEmptySet (th : Theory) where

open import abstract-set-theory.Prelude

open Theory th renaming (∅ to ∅ˢ)
open import Axiom.Set.Map th

record HasEmptySet (A : Type) : Type where
  field
    ∅ : A

open HasEmptySet ⦃...⦄ public

instance
  HasEmptySet-Set : {A : Type} → HasEmptySet (Set A)
  HasEmptySet-Set = record { ∅ = ∅ˢ }

  HasEmptySet-Map : {A B : Type} → HasEmptySet (Map A B)
  HasEmptySet-Map = record { ∅ = ∅ᵐ }