[Agda] universum levels

[Ulf Norell]

>  Is it true that each level universum is
>>                                           U(l) = all types of level <= l
>> ?
>>
>
> Yes.


Well, we would like this to be true, but in fact it is not. What is true is

  U(l) = all types of level = l

What you can do is embed a type from a lower lever into a higher level using
a wrapper datatype. For instance

data Embed {a} (A : Set a) : Set (suc a) where
  embed : A -> Embed A

In the library this is called Lift, I believe, and it has a more general
type.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140626/05be7ed4/attachment.html