{-# OPTIONS --safe #-}

open import Axiom.Set using (Theory)

module Class.HasSingleton (th : Theory) where

open Theory th renaming (Set to ℙ_; ❴_❵ to ❴_❵ˢ)

open import Axiom.Set.Map th
open import abstract-set-theory.Prelude

record HasSingleton (A B : Type) : Type where
  field
    ❴_❵ : A → B

open HasSingleton ⦃...⦄ public

instance
  HasSingletonSet-Set : {A : Type} → HasSingleton A (ℙ A)
  HasSingletonSet-Set = record { ❴_❵ = ❴_❵ˢ }

  HasSingletonSet-Map : {A B : Type} → HasSingleton (A × B) (Map A B)
  HasSingletonSet-Map = record { ❴_❵ = ❴_❵ᵐ }