{-# OPTIONS --safe --no-import-sorts #-}
 
open import Axiom.Set
 
module Class.IsSet (th : Theory) where
 
open Theory th renaming (_∈_ to _∈ᵗ_; _∉_ to _∉ᵗ_)
 
import Axiom.Set.Rel th as Rel
open import Axiom.Set.Map th as Map
open import Axiom.Set.TotalMap th as TotalMap
open import Data.Product
open import abstract-set-theory.Prelude
 
private variable A B X : Type
 
record IsSet (A B : Type) : Type where
  field
    toSet : A → Set B
 
  infix  _∈_ _∉_
  _∈_ _∉_ : B → A → Type
  a ∈ X = a ∈ᵗ (toSet X)
  a ∉ X = a ∉ᵗ (toSet X)
 
open IsSet ⦃...⦄ public
 
infix  All-syntax
All-syntax : ∀ {A X} ⦃ _ : IsSet X A ⦄ → (A → Type) → X → Type
All-syntax P X = All P (toSet X)
syntax All-syntax (λ x → P) l = ∀[ x ∈ l ] P
 
infix  Ex-syntax
Ex-syntax : ∀ {A X} ⦃ _ : IsSet X A ⦄ → (A → Type) → X → Type
Ex-syntax P X = Any P (toSet X)
syntax Ex-syntax (λ x → P) l = ∃[ x ∈ l ] P
 
module _ ⦃ _ : IsSet X (A × B) ⦄ where
  dom : X → Set A
  dom = Rel.dom ∘ toSet
 
  range : X → Set B
  range = Rel.range ∘ toSet
 
instance
  IsSet-Set : IsSet (Set A) A
  IsSet-Set .toSet A = A
 
  IsSet-Map : IsSet (Map A B) (A × B)
  IsSet-Map .toSet = _ˢ
 
  IsSet-TotalMap : IsSet (TotalMap A B) (A × B)
  IsSet-TotalMap .toSet = TotalMap.rel