[Agda] universum levels

[Abhishek Anand]

>
>
> Now, for  S, T  : Set l,
>
> build all type expressions from  S and T  by repeatedly applying the
> constructors  ×, →, ⊍.
>
> Probably, each of these types is in  Set l.
> Right?
>
> Yes. A universe is closed under those type constructors.


>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140626/c1e66e9c/attachment.html