[Agda] Proposed notation for universe polymorphism

[Andreas Abel]

To spin Andrea's idea further, we could make an overloaded "El" which 
has the internal workings of the following type class (not official Agda):

record ToType {a} {A : Set a} (a : A) : Setω where
   field toType : a → Setω

instance
   setToType : ∀{ℓ} → ToType (Set ℓ)
   setToType .ToType.toType A = A

   levelToType : ToType Level
   levelToType .ToType.toType ℓ = Set ℓ

   natToType : ToType Nat
   natToType .ToType.toType n = Fin n

You could then even write

   foo : (n : Nat) (i : n) -> ...

On 06.07.2017 12:07, Andrea Vezzosi 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
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/