{-# OPTIONS --type-in-type #-}
module TypeInType ( Void : Set ) where

open import Data.Bool

¬_ : Set -> Set
¬ x = x -> Void
record Tree : Set where
  constructor sup
  field
    a : Set
    f : a -> Tree
open Tree

open import Relation.Binary.PropositionalEquality
normal : Tree -> Set
normal t = (y : a t) -> ¬ (f t y ≡ sup (a t) (f t))

open import Data.Product

nt : Set
nt = ∃ normal

p : nt -> Tree
p = proj₁

q : (y : nt) -> normal (p y)
q = proj₂

r : Tree
r = sup nt p

lemma : normal r
lemma y z = subst (\ py -> ((y' : a py) → f py y' ≡ py → Void)) z (q y) y z

russel : Void
russel = lemma (r , lemma) refl

lemmag : (g : Void -> Void) -> normal r
lemmag g y z = g (lemma y z)

russelg : (Void -> Void) -> Void
russelg g = lemmag g (r , lemmag g) refl