The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hi David,

On Sep 14, 2010, at 3:49 PM, David Leduc wrote:
> 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!!

:-)

> > 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?

This is MiniAgda code (which is slightly different from Agda in  
Syntax). From this declaration you get:

T : (i : Size) -> Set $i
inn : [i : Size] -> Set i -> T i
out : [i : Size] -> T i -> Set i

"out", the destructor, is not needed.  Bracketed quantification [i :  
Size] -> ... is irrelevant quantification a la Barras/Bernardo (ICC).

> > 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?

Yes, you could also write

  let U : (i : Size) -> T $i
    = \ i -> inn $i (T i)

> I'm surprised by the $i in the type of U. Shouldn't it be the  
> successor of $i???

It type-checks:

  T i : Set $i
  inn $i (T i) : T $i

$i means "successor of i".

> Why do you pass two arguments to 'inn' while according to its
> definition it appears to take only one?

MiniAgda's "data" is like the "Inductive" definition in Coq.  The  
parameters (i:Size) are added to the constructor type.

Cheers,
Andreas

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/