<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div id="yiv6132914308"><div><div style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255); font-family: arial, helvetica, sans-serif; font-size: 10pt; "><div id="yiv6132914308yui_3_7_2_32_1372369622169_55"><span id="yiv6132914308yui_3_7_2_32_1372369622169_76">I've certainly run into issues with levels. A good example is an implementation of Scott/Church encodings. You can define the encoding, but trying to define simple things like addition becomes difficult if not impossible, from what I can tell.</span></div><div id="yiv6132914308yui_3_7_2_32_1372369622169_57"></div><div id="yiv6132914308yui_3_7_2_32_1372369622169_59">&nbsp;</div><div>- darryl<br></div>  <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; " id="yiv6132914308yui_3_7_2_32_1372369622169_65" class="yiv6132914308yui_3_7_2_32_1372369622169_64"> <div
 style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; " class="yiv6132914308yui_3_7_2_32_1372369622169_67"> <div dir="ltr"> <hr size="1">  <font size="2" face="Arial"> <b><span style="font-weight:bold;">From:</span></b> Guillaume Brunerie &lt;guillaume.brunerie@gmail.com&gt;<br> <b><span style="font-weight:bold;">To:</span></b>
 Andreas Abel &lt;andreas.abel@ifi.lmu.de&gt; <br><b><span style="font-weight:bold;">Cc:</span></b> agda list &lt;agda@lists.chalmers.se&gt; <br> <b><span style="font-weight:bold;">Sent:</span></b> Thursday, June 27, 2013 10:38 AM<br> <b><span style="font-weight:bold;">Subject:</span></b> Re: [Agda] More universe polymorphism<br> </font> </div> <div class="yiv6132914308y_msg_container"><br>Le 27 juin 2013 01:01, "Andreas Abel" &lt;<a rel="nofollow" ymailto="mailto:andreas.abel@ifi.lmu.de" target="_blank" href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt; a écrit :<br>&gt;<br>&gt; A minor reason for small level is Agda's built-in mechanism, where a Level is a built-in postulate<br>&gt;<br>&gt;&nbsp;  Level : Set<br>&gt;<br>&gt; Of course, this reason is minor because we could just have pragma<br>&gt;<br>&gt;&nbsp;  {-# BUILTIN LEVEL Level #-}<br>&gt;<br>&gt; without postulating Level first.<br>&gt;<br>&gt; I don't think there is any
 theoretical reason why Level should be
 small.&nbsp; Your suggested level supremum<br>&gt;<br>&gt;&nbsp;  sup : {i : Level}{A : Set i} (j : A -&gt; Level) -&gt; Level<br>&gt;<br>&gt; could interpreted as "constructor" with the usual structural ordering<br>&gt;<br>&gt;&nbsp;  j a &lt;= sup j.<br>&gt;<br>&gt; What would be an application for transfinite levels?<br><br>No idea, it just seems less ad-hoc than the current restriction and<br>not more difficult to implement (and hopefully consistent).<br>For instance it gives some kind of replacement: every small collection<br>of small things is small (which is not the case in Agda currently<br>because the sequence of the first omega universes is a small<br>collection of small things which is not small).<br><br>Maybe there will be a problem with equality between levels not being<br>well-behaved, though…<br><br>Cheers,<br>Guillaume<br><br>&gt; Cheers,<br>&gt; Andreas<br>&gt;<br>&gt;<br>&gt;<br>&gt; On 26.06.13 9:14 PM, Guillaume Brunerie
 wrote:<br>&gt;&gt;<br>&gt;&gt; Hi all,<br>&gt;&gt;<br>&gt;&gt; Quick recall of Agda’s universe polymorphism:<br>&gt;&gt;<br>&gt;&gt; There is a type Level of universe levels together with the following constants:<br>&gt;&gt;<br>&gt;&gt; zero : Level<br>&gt;&gt; suc : Level -&gt; Level<br>&gt;&gt; max : Level -&gt; Level -&gt; Level<br>&gt;&gt;<br>&gt;&gt; For every i : Level, there is a universe Set i, which is also a term<br>&gt;&gt; of type Set (suc i).<br>&gt;&gt; A dependent product (x : A) -&gt; B x such that A : Set i and B x : Set j<br>&gt;&gt; for all x : A is of type Set (max i j) (note that j cannot depend on<br>&gt;&gt; x, it has to be uniform).<br>&gt;&gt; Moreover, the type of universe levels Level is itself small (of type Type zero).<br>&gt;&gt;<br>&gt;&gt;<br>&gt;&gt; Why is Level required to be small?<br>&gt;&gt;<br>&gt;&gt; If we drop this requirement, it seems to me that we could extend max<br>&gt;&gt; so that we can get the maximum
 of any small family of universe levels,<br>&gt;&gt; i.e. have some max2 of type:<br>&gt;&gt;<br>&gt;&gt; max2 : (i : Level) (A : Set i) (j : A -&gt; Level) -&gt; Level<br>&gt;&gt;<br>&gt;&gt; Then a dependent product (x : A) -&gt; B x where A : Set i and B x : Set<br>&gt;&gt; (j x) would be of type Set (max2 i A j), so there is no "uniformity of<br>&gt;&gt; levels" restriction anymore, the only restriction is that the domain<br>&gt;&gt; and the codomain(s) are small.<br>&gt;&gt; You need the condition that Level is not small, or else you would be<br>&gt;&gt; able to define the max of all levels, which is likely to cause some<br>&gt;&gt; trouble.<br>&gt;&gt;<br>&gt;&gt; Such universe polymorphism would permit to define a lot of new<br>&gt;&gt; universes, indexed by a lot of big countable ordinals (maybe up to the<br>&gt;&gt; Feferman–Schütte ordinal?)<br>&gt;&gt;<br>&gt;&gt; Does that make sense? Is that consistent?<br>&gt;&gt; Did I miss something
 obvious?<br>&gt;&gt; I think there was something requiring Level to be small, but I don’t<br>&gt;&gt; remember what it is.<br>&gt;&gt;<br>&gt;&gt; Guillaume<br>&gt;&gt; _______________________________________________<br>&gt;&gt; Agda mailing list<br>&gt;&gt; <a rel="nofollow" ymailto="mailto:Agda@lists.chalmers.se" target="_blank" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>&gt;&gt; <a rel="nofollow" target="_blank" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>&gt;&gt;<br>&gt;<br>&gt; --<br>&gt; Andreas Abel&nbsp; &lt;&gt;&lt;&nbsp; &nbsp; &nbsp; Du bist der geliebte Mensch.<br>&gt;<br>&gt; Theoretical Computer Science, University of Munich<br>&gt; Oettingenstr. 67, D-80538 Munich, GERMANY<br>&gt;<br>&gt; <a rel="nofollow" ymailto="mailto:andreas.abel@ifi.lmu.de" target="_blank" href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>&gt; <a
 rel="nofollow" target="_blank" href="http://www2.tcs.ifi.lmu.de/~abel/">http://www2.tcs.ifi.lmu.de/~abel/</a><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></div> </div> </div>  </div></div></div></div></body></html>