The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Quoting Dan Doel 
<dan.doel AT gmail.com>:

> On Monday 13 September 2010 9:05:42 am Randy Pollack wrote:
>
> > It seems that Agda has some experimental feature of explicit
> > (outermost?) quantification over universe levels that should be looked
> > into.
>
> I don't know what you mean by "outermost".

Universe polymorphism is analagous to Hindley-Milner type  
polymorphism; i.e. outermost (implicit) quantification.

Randy


--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.