Re: [Agda] Level ω

[Andreas Abel]

On Sep 26, 2010, at 9:09 AM, David Leduc wrote:

> Andreas wrote:
>> Can't you do
>>
>> data T (max : Level) : Stream (BoundedLevel max) -> Set (suc max)  
>> where
>> makeT : (ls : Stream (BoundedLevel max)) -> Set max -> T max (tail  
>> ls)
>>
>> and then define a smart constructor
>>
>> makeT' : (ls : Stream (BoundedLevel max)) -> Set (Carrier (head  
>> ls)) ->
>>  T max (tail ls)
>>
>> that does the necessary liftings?
>
> Assuming that I have proved
>
>  max-is-max : (max : Level)(ls : Stream (BoundedLevel max)) ->
>    max ⊔ Carrier (head ls) ≡ max
>
> I cannot use it in the definition of makeT' because when I try do  
> destruct p in
>
>  makeT' max ls s with (max-is-max max ls)
>  makeT' max ls s | p = {!!}
>
> Agda raises an error
>
>  Cannot pattern match on constructor refl, since the inferred
>  indices [max' ⊔ Carrier (head ls')] cannot be unified with the
>  expected indices [max'] for some ls', max'
>  when checking that the expression ? has type T max (tail ls)
>
> Is it my mistake, or a limitation of Agda?

This is not how "with" can be used.

You could "with" more sucessfully if  the type of makeT' mentioned  
"max \sup (Carrier head ls)", then it could be rewritten by max-is-max  
to "max".

Anyway, I was more thinking in the direction that makeT' does the  
necessary liftings by considering all possible cases of "max" and  
"Carrier (head ls)".

All this should be much easier with cumulative universes, but I cannot  
promise you when they will be in Agda.

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/