[Agda] Proposed notation for universe polymorphism

[Martin Escardo]

(Yes, that's the idea. This is just new proposed notation, not new 
semantics. M.)

On 06/07/17 12:07, sanzhiyan at gmail.com wrote:
> Maybe this could work by having an implicit coercion from Level to
> "types", then you'd just have to rename Level into Universe to be able
> to write the second version.
> 
> On Thu, Jul 6, 2017 at 12:40 AM, Martín Hötzel Escardó
> <m.escardo at cs.bham.ac.uk> wrote:
>> Consider, for example, the Agda type
>>
>>     (I j : Level) -> Set i -> Set j -> Set(i\/j)
>>
>> e.g. for the sum of two types.
>>
>> I would like to, alternatively, write this type as follows:
>>
>>    (U V : Universe) -> U -> V -> U \/ V
>>
>> Instead of thinking of universe levels, I am thinking of universes
>> themselves.
>>
>> So then U \/ V is the least universe containing both U and V.
>>
>> In particular, this notation works well with for example univalent type
>> theory as in the HoTT book.
>>
>> This should not only make some definitions more concise and readable, but
>> also mathematically more intuitive.
>>
>> There are two pieces of notation missing in this proposal, for the first
>> universe and for the successor of a universe.
>>
>> I would like Agda to allow me to think and write in this way.
>>
>> Best, Martin
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe