{-#  OPTIONS --type-in-type #-}
{- 
  Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Lecture 20: Russell's paradox

  In this lecture we show that it is inconsistent to have
  Set:Set. Luckily, Agda is aware of this and indeed 
  Set=Set₀ : Set₁ : Set₂ : ...
  (this is called a predicative hierarchy).
  But with the pragma on top if this file, Agda will accept that
  Set:Set which makes it possible to derive Russell's paradox.
-}
module l20 where

open import Data.Nat
open import Data.Bool
open import Data.Unit
open import Data.Product
open import Data.Empty
open import Relation.Binary.PropositionalEquality

{- Russell's paradox: If there is a set of all sets then we can also
   construct the set R of all sets which do not contain themselves

   R = { X : Set | X ∉ X }

   Now if R∈R then R∉R and vice versa, which is inconsistent.

   However, we cannot replace ∈ by : because : is not a predicate (but
   it is a judgement. So to be able to encode Russell's paradox we
   first have to define sets in the sense of Set Theory which have a 
   predicate ∈. We do this by defining a type of trees we call M (for
   Menge = Set in german).
-}

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

{- Note that the definition of M already exploits Set : Set, because
   the constructor m has an argument I which is "too large".
-}

{- We can define some basic sets. Note that I use [..] for the names
   of sets because {..} are reserved symbols. -}

-- the empty set
 : M
 = m  ⊥-elim

-- the set containing the empty set
[∅] : M
[∅] = m   _  )

-- the set containing the empty set and the set containing the empty set
[∅,[∅]] : M
[∅,[∅]] = m Bool  x  if x then  else [∅])

{- We can now define ∈ (and ∉ as a predicates: -}
_∈_ : M  M  Set
a  m I f = Σ I  i  a  f i)

_∉_ : M  M  Set
a  b = (a  b)  

{- and define the set R: -}
R : M
R = m (Σ M  a  a  a)) proj₁

{- Indeed, every set which is in R does not contain itself -}
lem-1 :  {X}  X  R  X  X
lem-1 ((Y , Y∉Y) , refl) = Y∉Y

{- And every set which does not contain intself is in R -}
lem-2 :  {X}   X  X  X  R
lem-2 {X} X∉X = (X , X∉X) , refl

{- Now lem-1 already shows that R does not contain itself -}
lem-3 : R  R
lem-3 R∈R = lem-1 R∈R R∈R

{- and from this we can derive a contradiction -}
contr : 
contr = lem-3 (lem-2 lem-3)

{- What happens if we try to evaluate contr. ? -}