[Agda] How to formalize 'there exists a set' phrase?

[Dan Doel]

On Friday 09 July 2010 5:55:03 pm Dan Doel wrote:
> (I'm unsure if you could just use (Z {i} -> Set), and have
> everything happen to live in either Set or Set1; perhaps that's an
> option).

It occurred to me that this will not work, because Z {i} : Set (suc i), so in 
a predicative theory, Z {i} -> J has type, at lowest, Set (suc i). This means 
'sup (Z {i} -> Set) ...' can only inhabit Z {suc i} or above, so we still use 
the entire universe hierarchy. A monomorphic example would be:

  data Z : Set2 where
    sup : (I : Set1) -> (I -> Z) -> Z

  Power : Z -> Z
  Power (sup I f) = sup (Z -> Set) ? -- error

So, the inductive-recursive universe remains the best shot, I think (probably 
not surprising).

-- Dan