<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.&nbsp; 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'.&nbsp; To be more precise, I
      sometimes want a Setoid S whose carrier set C : Set is such that I
      have a function interp : C -&gt; Set.&nbsp; Basically I want to
      interpret C as a set-of-sets in Set.&nbsp; Another way to see it is
      that C is formed from those sets whose power-set is
      representable.&nbsp; 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.&nbsp; 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>&nbsp;</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">&lt;carette@mcmaster.ca&gt;</a><br>
                <b><span style="font-weight: bold;">To:</span></b> Agda
                <a class="moz-txt-link-rfc2396E" href="mailto:Agda@lists.chalmers.se">&lt;Agda@lists.chalmers.se&gt;</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?&nbsp; [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.&nbsp; 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.&nbsp; This would seem to
            indicate that, 'in the wild', Set_2 is all that is really
            needed.&nbsp; 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>