<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"> </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 <guillaume.brunerie@gmail.com><br> <b><span style="font-weight:bold;">To:</span></b>
Andreas Abel <andreas.abel@ifi.lmu.de> <br><b><span style="font-weight:bold;">Cc:</span></b> agda list <agda@lists.chalmers.se> <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" <<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>> a écrit :<br>><br>> A minor reason for small level is Agda's built-in mechanism, where a Level is a built-in postulate<br>><br>> Level : Set<br>><br>> Of course, this reason is minor because we could just have pragma<br>><br>> {-# BUILTIN LEVEL Level #-}<br>><br>> without postulating Level first.<br>><br>> I don't think there is any
theoretical reason why Level should be
small. Your suggested level supremum<br>><br>> sup : {i : Level}{A : Set i} (j : A -> Level) -> Level<br>><br>> could interpreted as "constructor" with the usual structural ordering<br>><br>> j a <= sup j.<br>><br>> 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>> Cheers,<br>> Andreas<br>><br>><br>><br>> On 26.06.13 9:14 PM, Guillaume Brunerie
wrote:<br>>><br>>> Hi all,<br>>><br>>> Quick recall of Agda’s universe polymorphism:<br>>><br>>> There is a type Level of universe levels together with the following constants:<br>>><br>>> zero : Level<br>>> suc : Level -> Level<br>>> max : Level -> Level -> Level<br>>><br>>> For every i : Level, there is a universe Set i, which is also a term<br>>> of type Set (suc i).<br>>> A dependent product (x : A) -> B x such that A : Set i and B x : Set j<br>>> for all x : A is of type Set (max i j) (note that j cannot depend on<br>>> x, it has to be uniform).<br>>> Moreover, the type of universe levels Level is itself small (of type Type zero).<br>>><br>>><br>>> Why is Level required to be small?<br>>><br>>> If we drop this requirement, it seems to me that we could extend max<br>>> so that we can get the maximum
of any small family of universe levels,<br>>> i.e. have some max2 of type:<br>>><br>>> max2 : (i : Level) (A : Set i) (j : A -> Level) -> Level<br>>><br>>> Then a dependent product (x : A) -> B x where A : Set i and B x : Set<br>>> (j x) would be of type Set (max2 i A j), so there is no "uniformity of<br>>> levels" restriction anymore, the only restriction is that the domain<br>>> and the codomain(s) are small.<br>>> You need the condition that Level is not small, or else you would be<br>>> able to define the max of all levels, which is likely to cause some<br>>> trouble.<br>>><br>>> Such universe polymorphism would permit to define a lot of new<br>>> universes, indexed by a lot of big countable ordinals (maybe up to the<br>>> Feferman–Schütte ordinal?)<br>>><br>>> Does that make sense? Is that consistent?<br>>> Did I miss something
obvious?<br>>> I think there was something requiring Level to be small, but I don’t<br>>> remember what it is.<br>>><br>>> Guillaume<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>> --<br>> Andreas Abel <>< Du bist der geliebte Mensch.<br>><br>> Theoretical Computer Science, University of Munich<br>> Oettingenstr. 67, D-80538 Munich, GERMANY<br>><br>> <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>> <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>