Russell's paradox

Russell.agda

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

open import Data.Empty
open import Data.Product
open import Relation.Nullary hiding (yes; no)
open import Relation.Binary.PropositionalEquality

-- Based on Robert Dockins's Coq reorganization of Chad E Brown's proof of Russell's paradox

data ⟨Set⟩ : Set where
  sets : {X : Set} (f : X → ⟨Set⟩) → ⟨Set⟩

data _∈_ : ⟨Set⟩ → ⟨Set⟩ → Set where
  includes : {X : Set} (f : X → ⟨Set⟩) (x : X) → f x ∈ sets f

invert : ∀ {x X} {f : X → ⟨Set⟩} → x ∈ sets f → ∃ (λ y → x ≡ f y)
invert (includes f y) = y , refl

RT = Σ[ x ∶ ⟨Set⟩ ] (¬ x ∈ x)

russell : ⟨Set⟩
russell = sets {RT} proj₁

no : russell ∈ russell → ⊥
no r with invert r
no r | (_ , f) , eq rewrite eq = f r

yes : russell ∈ russell
yes = includes proj₁ (, no)

paradox : ⊥
paradox = no yes