Russell's Paradox in Agda — taken from http://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html

Russell-Paradox.agda

{-#  OPTIONS --type-in-type #-}

-- Taken from http://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html

module _ where

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

data ⊥ : Set where

ex-falso-quodlibet : {A : Set} → ⊥ → A
ex-falso-quodlibet ()

data M : Set where
  m : (I : Set) → (I → M) → M

∅ : M
∅ = m ⊥ ex-falso-quodlibet

[∅] : M
[∅] = m ⊤ (λ _ → ∅)

[∅,[∅]] : M
[∅,[∅]] = m Two choose
  where
    data Two : Set where
      ff tt : Two
    choose : Two → M
    choose ff = ∅
    choose tt = [∅]

record Pair {A : Set} (B : A → Set) : Set where
  constructor pair
  field
    fst : A
    snd : B fst

_∈_ : M → M → Set
a ∈ m I f = Pair (λ x → a ≡ f x)

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

R : M
R = m (Pair (λ x → x ∉ x)) Pair.fst

in-R-not-in-self : ∀ {X} → X ∈ R → X ∉ X
in-R-not-in-self (pair (pair X X∉X) refl) = X∉X

not-in-self-in-R : ∀ {X} → X ∉ X → X ∈ R
not-in-self-in-R {X} X∉X = pair (pair X X∉X) refl

R∉R : R ∉ R
R∉R R∈R = in-R-not-in-self R∈R R∈R

contradiction : ⊥
contradiction = R∉R (not-in-self-in-R R∉R)