cset.agda

module _ where

-- Constructive Set
data CSet {A : Set} : (A → Set) → Set where
  ⟨_⟩  : (p : A → Set) → CSet p

data _∈_ {A : Set} {p : A → Set} (x : A) (S : CSet p) : Set where
  ∈-pf : p x → x ∈ S

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

-- x is an element of the set containing elements equal to x
triv₁ : {A : Set} (x : A) → x ∈ ⟨ (λ y → x ≡ y) ⟩
triv₁ _ = ∈-pf refl