<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">I would be quite surprised if it were
so. I was more going for a rough analogy.<br>
<br>
What I do find I am missing is a nice way to tell Agda that I want
certain inhabitants of Set0 to be 'small'. To be more precise, I
sometimes want a Setoid S whose carrier set C : Set is such that I
have a function interp : C -> Set. Basically I want to
interpret C as a set-of-sets in Set. Another way to see it is
that C is formed from those sets whose power-set is
representable. As far as I can tell, in such a situation C really
ought to be in Set_{-1}, and assuming we have a 'small' equality
as well, then Setoid S would be in Set0, not Set1. In the codes I
have, this would definitely help keep universe sizes way down.<br>
<br>
Jacques<br>
<br>
On 12-12-23 11:25 PM, Darryl wrote:<br>
</div>
<blockquote
cite="mid:1356323134.13980.YahooMailNeo@web163806.mail.gq1.yahoo.com"
type="cite">
<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>- 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 face="Arial" size="2">
<hr size="1"> <b><span style="font-weight:bold;">From:</span></b>
Jacques Carette <a class="moz-txt-link-rfc2396E" href="mailto:carette@mcmaster.ca"><carette@mcmaster.ca></a><br>
<b><span style="font-weight: bold;">To:</span></b> Agda
<a class="moz-txt-link-rfc2396E" href="mailto:Agda@lists.chalmers.se"><Agda@lists.chalmers.se></a> <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 moz-do-not-send="true"
ymailto="mailto:Agda@lists.chalmers.se"
href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a moz-do-not-send="true"
href="https://lists.chalmers.se/mailman/listinfo/agda"
target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
</div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>