The Coq mailing list

[David Leduc <david.leduc6 AT googlemail.com>]

HI Andreas,

Andreas Abel 
<andreas.abel AT ifi.lmu.de>
 wrote:
> During the Agda meeting which finished a week ago we started to add
> cumulativity

This looks like a very dynamic community!!

> As of now, you can play with explicit universe polymorphism and cumulativity
> in MiniAgda (see my homepage).  There your example looks like:

I'm not familiar with Agda's syntax.

> data T (i : Size) : Set $i
> { inn : (out : Set i) -> T i
> }

I guess 'inn' is for the 't' in my example.
What is 'out'? Why do you need it?

> fun U : (i : Size) -> T $i
> { U i = inn $i (T i)
> }

I guess it's a function definition by case analysis (here the only
case is 'i'), right?
I'm surprised by the $i in the type of U. Shouldn't it be the successor of 
$i???
Why do you pass two arguments to 'inn' while according to its
definition it appears to take only one?