<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div>That's a good point, yes. I wonder if there's a way to have level-pi types without being inconsistent then. probably not?</div><div><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">G, a level |-- A type a ===> G |- LPi a. A type ?n</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="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">This probably can't work, indeed.</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal;
"><span><br></span></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> Guillaume Brunerie <guillaume.brunerie@gmail.com><br> <b><span style="font-weight: bold;">To:</span></b> Darryl McAdams <psygnisfive@yahoo.com> <br><b><span style="font-weight: bold;">Cc:</span></b> Peter Hancock <hancock@spamcop.net>; "agda@lists.chalmers.se" <agda@lists.chalmers.se> <br> <b><span style="font-weight: bold;">Sent:</span></b> Monday, July 1, 2013 3:16 PM<br> <b><span style="font-weight: bold;">Subject:</span></b> 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>Well, if you want to define a polymorphic function (polymorphic on all<br>small types, not restricted to some universe), you have to quantify<br>over all levels.<br>Or you can use typical ambiguity, but this is kind of cheating.<br>Maybe you could instead have a notion of universal quantification over<br>all universes which would be a primitive notion, distinct from the<br>usual Pi types. Various people were talking about that at the IAS this<br>year but I don’t know if anyone tried to write down the rules.<br><br>But if having a type of universe levels is consistent and natural and<br>pretty, I don’t see why we should try to avoid it.<br><br>Guillaume<br><br>2013/7/1 Darryl McAdams <<a ymailto="mailto:psygnisfive@yahoo.com" href="mailto:psygnisfive@yahoo.com">psygnisfive@yahoo.com</a>>:<br>> Do levels really have to be things at all? If we think of
levels as<br>> merely/purely syntactic elements of the type theory, then it seems like the<br>> relational judgment "type_n" that Martin mentions would sidestep the issue<br>> entirely. Levels would no more exist in the model then ":" and<br>> "valid-context" do.<br>><br>> - darryl<br>><br>> ________________________________<br>> From: Peter Hancock <<a ymailto="mailto:hancock@spamcop.net" href="mailto:hancock@spamcop.net">hancock@spamcop.net</a>><br>> To: <a ymailto="mailto:agda@lists.chalmers.se" href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>> Sent: Monday, July 1, 2013 2:30 PM<br>> Subject: Re: [Agda] How does level polymorphism fit into a valid type<br>> theory? (from "More universe polymorphism")<br>><br>> On 01/07/2013 17:04, Martin Escardo wrote:<br>>> Ok, I understand, Guillaume. The crucial thing, in your formulation<br>>> below of transfinite universes, is that
Level is a type but cannot<br>>> 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. So, they don't live in any universe,<br>> at least not in the sense of a Grothendieck universe. 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. 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). Nobody knew what type they lived in, or what the<br>> level of that
type should be. 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>><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>