Total Paradoxes

{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

data ⊥ : Set where
⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()
data SET : Set where
  set : (X : Set) → (X → SET) → SET

∅ : SET
∅ = set ⊥ ⊥-elim

_∈_ : SET → SET → Set
a ∈ set X f = Σ X (λ x → a ≡ f x)

_∉_ : SET → SET → Set
a ∉ b = (a ∈ b) → ⊥

Δ : SET
Δ = set (Σ SET (λ s → s ∉ s)) fst

x∈Δ→x∉x : ∀ {X} → X ∈ Δ → X ∉ X
x∈Δ→x∉x ((Y , Y∉Y) , refl) = Y∉Y

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


Δ∉Δ : Δ ∉ Δ
Δ∉Δ prf = x∈Δ→x∉x prf prf

Δ∈Δ : Δ ∈ Δ
Δ∈Δ = x∉x→x∈Δ Δ∉Δ

russell : ⊥
russell = Δ∉Δ Δ∈Δ