<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>Is it strictly true that sets, classes, and conglomerates are equivalent to Set0, Set1, and Set2, respectively?</span></div><div></div><div> </div><div>- darryl<br></div> <div style="font-size: 10pt; font-family: arial, helvetica, sans-serif; "> <div style="font-size: 12pt; font-family: 'times new roman', 'new york', times, serif; "> <div dir="ltr"> <font size="2" face="Arial"> <hr size="1"> <b><span style="font-weight:bold;">From:</span></b> Jacques Carette <carette@mcmaster.ca><br> <b><span style="font-weight: bold;">To:</span></b> Agda <Agda@lists.chalmers.se> <br> <b><span style="font-weight: bold;">Sent:</span></b> Saturday, December 22, 2012 11:11 AM<br> <b><span style="font-weight: bold;">Subject:</span></b> [Agda] Highest Level seen?<br> </font> </div> <br>
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>_______________________________________________<br>Agda mailing list<br><a ymailto="mailto:Agda@lists.chalmers.se"
href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br> </div> </div> </div></body></html>