[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.
> 
> On 23.06.2014 11:02, Sergei Meshveliani wrote:
> > 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 ?
> 
> Well, you give the level yourself.
> 
> [..]


Thanks for your response.

Conserning  "give the level yourself":

if I give  level = 0  everywhere in the code, Agda will most probably
report an error of kind
                        zero < <some-level-expression>.

Then I set  <some-level-expression>  there. 
And Agda reports of
                      level-2 < <level-expression-2>  
in some other place.
I set  <level-expression-2>  there
(because I expect that it is better to set a minimal possible level
everywhere).
This process always converges, in my experience.
As Agda error-reports things like, for example,   l < l max (suc a),

I thought that starting with  level = 0  everywhere in the user program,
Agda can, in principle, find itself the minimal possible level
expressions to set everywhere.

Can it?

Thanks,

------
Sergei