<div dir="ltr"><p dir="ltr">Standard mathematics is also impredicative. The power set of a set is a set. This is not true in Agda.</p><p dir="ltr">There are also certain things one does in Agda that don't seem to be done explicitly in set theory via the hierarchy. For instance, it's not terribly far out to want a list of types, and for that we need to talk about the type of lists of types, which inhabits a higher universe. But a set or list of sets isn't necessarilly a very large object in set theory, and I doubt the class of all lists of sets (which surely is a proper class) is talked about much in set theory. One would probably avoid talking about the entire class, but work with the elements that are a) not big and b) exist independently of the entire class, in set theory. Similarly, one can manipulate sets and sets of sets and so on without mentioning the class of all sets at all in the theory.<br>
</p><p style>-- Dan</p>
<div class="gmail_quote">On Dec 22, 2012 11:12 AM, "Jacques Carette" <<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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]<br>
<br>
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?<br>
<br>
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...<br>
<br>
Jacques<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div>
</div>