{-# OPTIONS --without-K --type-in-type #-}
module russell where

open import sum
open import equality.core
open import sets.empty

-- a model of set theory
data U : Set where
  set : (I : Set) → (I → U) → U

-- a set is regular if it doesn't contain itself
regular : U → Set
regular (set I f) = (i : I) → ¬ (f i ≡ set I f)

-- Russell's set: the set of all regular sets
R : U
R = set (Σ U regular) proj₁

-- R is not regular
R-nonreg : ¬ (regular R)
R-nonreg reg = reg (R , reg) refl

-- R is regular
R-reg : regular R
R-reg (x , reg) p = subst regular p reg (x , reg) p

-- contradiction
absurd : ⊥
absurd = R-nonreg R-reg