[Agda] Highest Level seen?

[Nils Anders Danielsson]

On 2012-12-22 17:11, Jacques Carette wrote:
> 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...

I have used Set₃:

   http://www.cse.chalmers.se/~nad/listings/equality/Univalence-axiom.Isomorphism-implies-equality.Simple.html

I can't recall having used Set₄, and (at the time of writing) get zero
hits when I search for Set₄ using Google.

-- 
/NAD