[Agda] AIM 10 notes

[Robin Green]

At Sat, 19 Sep 2009 22:53:35 +0200,
Patrik Jansson wrote:
> 
> AIM 10 is over but some notes and slides have been collected on the wiki:
> 
>   http://wiki.portal.chalmers.se/agda/Main.AIMX

On universe polymorphism it is written:

     postulate
       ↑_ : ∀ {n} Set n → Set (suc n)
       ⇑_ : ∀ {n}{A : Set n} → A → ↑ A
       ⇓_ : ∀ {n}{A : Set n} → ↑ A → A

Are these going to be actual postulates, or are they going to be
(at least, in the case of the first two postulates)
automatically-applied implicit rules? I was hoping for the latter,
which was an earlier design and which is covered by
http://code.google.com/p/agda/issues/detail?id=182