<div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is it true that each level universum is<br>
                                          U(l) = all types of level &lt;= l<br>
?<br>
</blockquote>
<br></div>
Yes.</blockquote><div><br></div><div>Well, we would like this to be true, but in fact it is not. What is true is</div><div><br></div><div>  U(l) = all types of level = l</div><div><br></div><div>What you can do is embed a type from a lower lever into a higher level using</div>

<div>a wrapper datatype. For instance</div><div><br></div><div>data Embed {a} (A : Set a) : Set (suc a) where</div><div>  embed : A -&gt; Embed A</div><div><br></div><div>In the library this is called Lift, I believe, and it has a more general type.</div>

<div><br></div><div>/ Ulf</div></div></div></div>