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