[Agda] More universe polymorphism

Guillaume Brunerie guillaume.brunerie at gmail.com
Sat Jun 29 04:00:28 CEST 2013


On 2013/6/29 Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>
> On 29/06/13 02:13, Guillaume Brunerie wrote:
>>
>> (1) Why are you using this complicated f instead of \ i -> Set i,
>
> Because f has a type, but \ i -> Set i doesn't.

Yes it does, it’s (i : Level) -> Set (lsucc i).


More information about the Agda mailing list