russell.idris

data Set : Type where
    Comp : (Set -> Type) -> Set

elt : Set -> Set -> Type
elt (Comp f) = f

W : Set
W = Comp (\A => Not (A `elt` A))

Russell : Type
Russell = W `elt` W

{-
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 0.9.10.1
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Type checking russell.idris
*russell> Russell
^Cuser interrupt
-}