[Agda] AIM 10 notes

[Dan Doel]

On Sunday 20 September 2009 2:20:50 pm Robin Green wrote:
> 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

I must admit, I had similar hopes. I don't know much Coq, but it seems to have 
quite serviceable universe polymorphism, based around rules like:

  "Type" can be used in lieu of "Type[i]" when 'i's can be inferred
  If A : Type[i], and i < j, then A : Type[j] as well

Which seems to allow for not actually mentioning the indices much, even when 
multiple universe levels may be in play (as the solver is generally 
sufficient). Of course, that requires the indices and solver thereof to be 
more built-in, but I'm not sure that's unreasonable.

But, as I said, I don't know much Coq. Is there something problematic about 
the Coq implementation that the folks discussing universe polymorphism in Agda 
are attempting to avoid?

-- Dan