<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>Do levels really have to be things at all? If we think of levels as merely/purely syntactic elements of the type theory, then it seems like the relational judgment "type_n" that Martin mentions would sidestep the issue entirely. Levels would no more exist in the model then ":" and "valid-context" do.</span></div><div></div><div>&nbsp;</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-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <hr size="1">  <font size="2" face="Arial"> <b><span style="font-weight:bold;">From:</span></b> Peter Hancock

&lt;hancock@spamcop.net&gt;  <span style="font-weight: bold;">To: agda@lists.chalmers.se   <span style="font-weight: bold;">Sent: Monday, July 1, 2013 2:30 PM  <span style="font-weight: bold;">Subject: Re: [Agda] How does level polymorphism fit into a valid type theory?

        (from "More universe polymorphism")<br> </font> </div> <div class="y_msg_container"><br>On 01/07/2013 17:04, Martin Escardo wrote:<br>&gt; Ok, I understand, Guillaume. The crucial thing, in your formulation<br>&gt; below of transfinite universes, is that Level is a type but cannot<br>&gt; live in a universe, right? (So it doesn't have a type.)<br><br>In set theory, ordinals (that index the cumuluative hierarchy)<br>form a class, just like sets.&nbsp;  So, they don't live in any universe,<br>at least not in the sense of a Grothendieck universe.&nbsp; They are<br>"commensurate" with the notion of set itself.<br><br>The notion of "set" (or whatever you want to call it)<br>is inexpressible in Agda. That is why Martin-Lof (and G. Brunerie)<br>proposes a judgement form for it different from a : A.&nbsp; If Agda<br>had the notion of set, by the same token, it would have a coherent<br>notion of level.<br><br>One hundred years ago, we had Principia mathematica,

 which was a<br>ramified theory, with "levels" (short circuited by reducibility,<br>but never mind).&nbsp; Nobody knew what type they lived in, or what the<br>level of that type should be.&nbsp; It seems to me that in 100 years,<br>we have travelled precisely nowhere.<br><br>Hank<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>  </div></body></html>