[Agda] Highest Level seen?

[Jacques Carette]

I am curious about one point: what is the highest Level that has been 
seen in practice in an Agda development?  [Of course, one can 
artificially go arbitrarily high; by 'in practice', I mean in the course 
of developing some theory for the purposes of applications]

A lot of Agda is done in a level-polymorphic way.  What I mean by my 
question is then: how many suc's did you have to put in to make things 
go through?

In standard mathematics, when people worry about size, they tend to go 
with sets, classes, and super-classes (sometimes called conglomerates), 
and no higher.  This would seem to indicate that, 'in the wild', Set_2 
is all that is really needed.  Of course, given the sloppiness of 
standard mathematics, one wonders if what they do really does level-check...

Jacques