[Agda] Proposed notation for universe polymorphism

[Andrea Vezzosi]

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
>