{-# OPTIONS --safe #-}
module set-in-set where
-- Basically just a modified version of http://liamoc.net/posts/2015-09-10-girards-paradox.html
-- Some preliminaries, just to avoid any library imports
data _≡_ {ℓ : _} {A : Set ℓ} : A -> A -> Set where
    refl : ∀ {a} -> a ≡ a

record Σ (A : Set) (P : A -> Set) : Set where
    constructor _,_
    field
        proj₁ : A
        proj₂ : P proj₁
open Σ

data ⊥ : Set where

-- This shows the problem
WTF : Set₀
WTF = Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅
-- 18446744073709551615 = 2^64 - 1

-- The following is basically copying from the link
data SET : Set where
  set : (X : Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅) → (X → SET) → SET

_∈_ : 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)) proj₁

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 = (X , X∉X) , refl

falso : ⊥
falso = Δ∉Δ (x∉x→x∈Δ Δ∉Δ)