[Agda] implicit level arguments

[Serge D. Mechveliani]

People,
can you, please, explain about the  level arguments  style?

The Standard library lib-0.6 declares, for example,

  record _=>_ {c} (CБ┌│ CБ┌┌ : Container c) : Set c where ...      -- I

  record Semigroup c l : Set (suc (max c l)) where ...         -- II
  Group, RingWithOne ...  are in the same style of  II

  record Container (l : Level) : Set (suc l) where ...         -- III

  data Eq {a l} {A : Set a} (_~~_ : Rel A l) : ...             -- IV

(for this letter, I replace some math symbols).

My impression is that the level arguments should be implicit.
Because  
a) I suspect that levels are needed to differ between such collections 
   as sets and proper classes, and the like (right?),
b) in practical computation, one usually does not think of whether the
   data is of a set or of a proper class,
   (this is kind of a second class information).

Now, (I) hides the level,  II uses explicit levels, 
III uses an explicit level, and even adds  `: Level' 
and  `data Eq'  hides its two levels.

Is this put at random or by some systematic approach?
Can you, please, comment and advise?

Thanks,

------
Sergei