[Agda] Big indices for small types?

[Thorsten Altenkirch]

Hi Peter,

> Have you got a consistency proof (relative to set theory)?

Actually, it should be possible to model this in the calculus of  
constructions + universes (ECC). However, it seems to me that you  
would need the impredicative universe on top of the predicative  
hierarchy. But I think this is equivalent, isn't it?

I am suggesting to use Leibniz equality, I don't think that the  
inductive characterisation adds any strength.

> I don't have anything specific to say about your definition, except  
> that
> it goes against certain
> intuitions about "predicativity" (relating to concepts such as  
> "before",
> "after", "below", and "above").
> However, to me "predicativity" is a subjective notion, it's all in  
> your
> own mind, and not an objective concept, which is what really counts.

Ouch! Are there any "objective concepts" in Mathematics? I had the  
impression this has all to do with our mind. Isn't this what  
intuitionism is all about? I didn't know that you had become a bold  
Platonist?

Objective concepts: Kronecker suggested the natural numbers, otherwise  
you have to believe in some higher authority. Even the natural numbers  
are not really objective but based on a very broad agreement. My  
understanding of intuitionism (and hence predicativity) was that we  
carefully try to extend this agreement.

Classical reasoning is not based on "objective concepts" but on the  
assumption that "anything goes" unless somebody has fund a  
contradiction. Personally, I find this not only interlectually less  
satisfying than the intuitionist approach but also pragmatically less  
helpful, since a careful intuitionistic analysis often leads to better  
theories, imho.

> I propose the following plan of action when adding a new  
> construction to
> Martin-Löf type theory (Agda).
>
> 1. Prove it consistent relative to set theory
> 2. Give an informal but careful analysis why it is constructive,  
> that is,
> why it satisfies Martin-Löf's style meaning explanations.
> 3. Prove normalization and decidability of type-checking for the  
> extended
> system.

it seems we may have trouble at step 2.

Cheers,
Thorsten

> It's probably also important to have a good motivating example.
>
> Cheers,
> Peter
>
>> Just fiddling about with some ideas about stratification
>> and wondering if anyone has anything substantial to say
>> about definitions like
>>
>>   data EQ (S : Set1) : Set1 -> Set where
>>     REFL : EQ S S
>>
>> On the one hand, this doesn't exactly fit with the idea
>> of building the hierarchy up from below. On the other
>> hand, it doesn't actually store any big things inside
>> any small things.
>>
>> Of course, Agda 2's
>>
>>   data BEFORE : AFTER -> Set
>>
>> distinction isn't the usual parameter/index distinction,
>> as shown
>>
>>   data Lam (X : Set) : Set where
>>     var : X -> Lam X
>>     app : Lam X -> Lam X -> Lam X
>>     lam : Lam (Maybe X) -> Lam X
>>
>> Sizewise, it seems that anything goes as long as there's
>> no large payload.
>>
>> Is this well understood?
>>
>> Scares me.
>>
>> Cheers
>>
>> Conor
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.