[Agda] universum levels

[Sergei Meshveliani]

On Wed, 2014-06-25 at 21:30 +0200, Andreas Abel wrote:
> Levels are there to prevent Hurkens Paradox.  In particular,
> 
>    Set : Set
> 
> is inconsistent.
> 


Probably, this is like  the set/class of all sets in the axiomatic
classical set theory.

  T : Set₁
  T = Set

is type-checked, and  T : Set  is not.


> The "size" of sets (e.g. given by inaccessible cardinals).


Now, for  S, T  : Set l,

build all type expressions from  S and T  by repeatedly applying the
constructors  ×, →, ⊍.

Probably, each of these types is in  Set l.  
Right? 

Thanks,

------
Sergei