<br><div class="gmail_quote">On Fri, Sep 25, 2009 at 6:30 PM, Benja Fallenstein <span dir="ltr">&lt;<a href="mailto:benja.fallenstein@gmail.com">benja.fallenstein@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi Ulf,<br>
<div class="im"><br></div><div class="im">
&gt;   At present there is no way to lift types from one level to another, that<br>
&gt;   is, there is no function<br>
&gt;     lift : {i : Level} -&gt; Set i -&gt; Set (suc i)<br>
&gt;   This is likely to change at some point.<br>
<br>
</div>Does that mean that doing it manually using levels in data<br>
declarations is not / not yet possible? I.e.,<br>
<br>
data Lift {i : Level} (X : Set i) : (Set (suc i)) where<br>
  lift : X -&gt; Lift X<br>
<br>
Or does it just mean there&#39;s no built-in support?</blockquote><div><br></div><div>No built-in support. You can define the Lift datatype above.</div><div><br></div><div>/ Ulf</div></div>