[Agda] universum levels

[Sergei Meshveliani]

People,

I am writing a manual on a program written in Agda, and wonder:
what brief explanation words to set about an  universum level  
(l : Level) ?

I know only that 
(1) each type belongs to some universums,
(2) each universum has its level  l : Level,
(3) Level  has the operations  suc, _⊔_,
(4) Agda can show some level expression for each given type.

Is it true that for each type Agda finds a minimal universum level ?
Is it true that each level universum is 
                                         U(l) = all types of level <= l
?
It is true that 
           All types =  U(0) union U(suc 0) union U(suc $ suc 0) ...
?
Approximately and briefly, what notion does Level express?
Is it related to the relative algorithmic decidability or
enumerability? 

Thanks,

------
Sergei