<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>I've wondered on numerous occasions whether or not pure sets (ie no data declarations) gives a traditional iterated conception of set. I've never fully determined if the answer is yes or no. I think you might need Lift as the only data decl to get that, maybe? But the absence of pattern matching on types makes it useless.</span></div><div></div><div><br></div><div>- darryl<br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><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> Darryl <psygnisfive@yahoo.com> <br><b><span style="font-weight: bold;">Cc:</span></b> Agda <Agda@lists.chalmers.se> <br> <b><span style="font-weight: bold;">Sent:</span></b> Monday, December 24, 2012 8:39 AM<br> <b><span style="font-weight: bold;">Subject:</span></b> Re: [Agda] Highest Level seen?<br> </font> </div> <br>
<meta http-equiv="x-dns-prefetch-control" content="off"><div id="yiv1994827383">
<div>
<div class="yiv1994827383moz-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 type="cite">
<div style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255); font-size: 10pt; font-family: arial, helvetica, sans-serif; ">
<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 rel="nofollow" class="yiv1994827383moz-txt-link-rfc2396E" ymailto="mailto:carette@mcmaster.ca" target="_blank" href="mailto:carette@mcmaster.ca"><carette@mcmaster.ca></a><br>
<b><span style="font-weight:bold;">To:</span></b> Agda
<a rel="nofollow" class="yiv1994827383moz-txt-link-rfc2396E" ymailto="mailto:Agda@lists.chalmers.se" target="_blank" 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 rel="nofollow" ymailto="mailto:Agda@lists.chalmers.se" target="_blank" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a rel="nofollow" target="_blank" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
</div>
</div>
</div>
<br>
<fieldset class="yiv1994827383mimeAttachmentHeader"></fieldset>
<br>
<pre>_______________________________________________
Agda mailing list
<a rel="nofollow" class="yiv1994827383moz-txt-link-abbreviated" ymailto="mailto:Agda@lists.chalmers.se" target="_blank" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a rel="nofollow" class="yiv1994827383moz-txt-link-freetext" target="_blank" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</div>
</div><meta http-equiv="x-dns-prefetch-control" content="on"><br><br> </div> </div> </div></body></html>