<div>The development version now has (very experimental) support for (non-uniform) universe</div><div>polymorphism. At this stage there's no lifting between levels, but you can get quite far</div><div>without that. Some examples are in test/succeed/UniversePolymorphism.agda.</div>
<div><br></div><div>Happy hacking!</div><div><br></div><div>From the release notes:</div><div><br></div><div> To enable universe polymorphism give the flag --universe-polyorphism</div><div> on the command line, as an OPTIONS pragma (recommended) or set it in</div>
<div> the emacs mode options.</div><div><br></div><div> When universe polymorphism is enabled Set takes an argument which is</div><div> the universe level. For instance, the type of universe polymorphic identity</div><div>
is</div><div><br></div><div> id : {i : Level}{A : Set i} -> A -> A</div><div><br></div><div> The type Level is isomorphic to the unary natural numbers and should be</div><div> specified using the BUILTINs LEVEL, LEVELZERO, and LEVELSUC:</div>
<div><br></div><div> data Level : Set where</div><div> zero : Level</div><div> suc : Level -> Level</div><div> </div><div> {-# BUILTIN LEVEL Level #-}</div><div> {-# BUILTIN LEVELZERO zero #-}</div>
<div> {-# BUILTIN LEVELSUC suc #-}</div><div><br></div><div> There is an additional BUILTIN LEVELMAX for taking the maximum of two</div><div> levels:</div><div><br></div><div> max : Level -> Level -> Level</div>
<div> max zero m = m</div><div> max (suc n) zero = suc n</div><div> max (suc n) (suc m) = suc (max n m)</div><div><br></div><div> {-# BUILTIN LEVELMAX max #-}</div><div><br></div><div> The non-polymorphic universe levels Set, Set₁, .. are sugar for Set zero,</div>
<div> Set (suc zero), ..</div><div><br></div><div> At present there is no way to lift types from one level to another, that</div><div> is, there is no function</div><div><br></div><div> lift : {i : Level} -> Set i -> Set (suc i)</div>
<div><br></div><div> This is likely to change at some point.</div><div><br></div><div>/ Ulf</div>