[Agda] Highest Level seen?

[Darryl]

Is it strictly true that sets, classes, and conglomerates are equivalent to Set0, Set1, and Set2, respectively?

 
- darryl


________________________________
 From: Jacques Carette <carette at mcmaster.ca>
To: Agda <Agda at lists.chalmers.se> 
Sent: Saturday, December 22, 2012 11:11 AM
Subject: [Agda] Highest Level seen?
 
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
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121223/0f1b3892/attachment.html