{-# OPTIONS --type-in-type #-}
open import Data.Empty
open import Data.Product using (Σ ; proj₁ ; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
  
data set : Set where
  ⟨_∣_⟩ : (X : Set) → (X → set) → set

module _ where
  open import Data.Unit
  open import Data.Bool
  ∅ : set
  ∅ = ⟨ ⊥ ∣ ⊥-elim ⟩

  ⟨∅⟩ : set
  ⟨∅⟩ = ⟨ ⊤ ∣ (λ _ → ∅) ⟩

  ⟨∅,⟨∅⟩⟩ : set
  ⟨∅,⟨∅⟩⟩ = ⟨ Bool ∣ (λ {true → ∅ ; false → ⟨∅⟩}) ⟩

_∈_ : set → set → Set
A ∈ ⟨ X ∣ p ⟩ = Σ X (λ x → A ≡ p x)

_∉_ : set → set → Set
A ∉ B = A ∈ B → ⊥

R : set
R = ⟨ (Σ set (λ x → x ∉ x)) ∣ proj₁ ⟩

x∈R→x∉x : ∀ {x} → x ∈ R → x ∉ x
x∈R→x∉x ((x , x∉x) , refl) = x∉x

x∉x→x∈R : ∀ {x} → x ∉ x → x ∈ R
x∉x→x∈R {x} x∉x = (x , x∉x) , refl

R∉R : R ∉ R
R∉R p = x∈R→x∉x p p

uhoh : ⊥
uhoh = R∉R (x∉x→x∈R R∉R)