[Agda] More universe polymorphism

Darryl McAdams psygnisfive at yahoo.com
Fri Jun 28 01:09:50 CEST 2013

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.
- darryl

 From: Guillaume Brunerie <guillaume.brunerie at gmail.com>
To: Andreas Abel <andreas.abel at ifi.lmu.de> 
Cc: agda list <agda at lists.chalmers.se> 
Sent: Thursday, June 27, 2013 10:38 AM
Subject: Re: [Agda] More universe polymorphism

Le 27 juin 2013 01:01, "Andreas Abel" <andreas.abel at ifi.lmu.de> a écrit :
> A minor reason for small level is Agda's built-in mechanism, where a Level is a built-in postulate
>   Level : Set
> Of course, this reason is minor because we could just have pragma
>   {-# BUILTIN LEVEL Level #-}
> without postulating Level first.
> I don't think there is any theoretical reason why Level should be
 small.  Your suggested level supremum
>   sup : {i : Level}{A : Set i} (j : A -> Level) -> Level
> could interpreted as "constructor" with the usual structural ordering
>   j a <= sup j.
> What would be an application for transfinite levels?

No idea, it just seems less ad-hoc than the current restriction and
not more difficult to implement (and hopefully consistent).
For instance it gives some kind of replacement: every small collection
of small things is small (which is not the case in Agda currently
because the sequence of the first omega universes is a small
collection of small things which is not small).

Maybe there will be a problem with equality between levels not being
well-behaved, though…


> Cheers,
> Andreas
> On 26.06.13 9:14 PM, Guillaume Brunerie
>> Hi all,
>> Quick recall of Agda’s universe polymorphism:
>> There is a type Level of universe levels together with the following constants:
>> zero : Level
>> suc : Level -> Level
>> max : Level -> Level -> Level
>> For every i : Level, there is a universe Set i, which is also a term
>> of type Set (suc i).
>> A dependent product (x : A) -> B x such that A : Set i and B x : Set j
>> for all x : A is of type Set (max i j) (note that j cannot depend on
>> x, it has to be uniform).
>> Moreover, the type of universe levels Level is itself small (of type Type zero).
>> Why is Level required to be small?
>> If we drop this requirement, it seems to me that we could extend max
>> so that we can get the maximum
 of any small family of universe levels,
>> i.e. have some max2 of type:
>> max2 : (i : Level) (A : Set i) (j : A -> Level) -> Level
>> Then a dependent product (x : A) -> B x where A : Set i and B x : Set
>> (j x) would be of type Set (max2 i A j), so there is no "uniformity of
>> levels" restriction anymore, the only restriction is that the domain
>> and the codomain(s) are small.
>> You need the condition that Level is not small, or else you would be
>> able to define the max of all levels, which is likely to cause some
>> trouble.
>> Such universe polymorphism would permit to define a lot of new
>> universes, indexed by a lot of big countable ordinals (maybe up to the
>> Feferman–Schütte ordinal?)
>> Does that make sense? Is that consistent?
>> Did I miss something
>> I think there was something requiring Level to be small, but I don’t
>> remember what it is.
>> Guillaume
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
Agda mailing list
Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130627/d9bda76a/attachment.html

More information about the Agda mailing list