[Agda] Size of propositional equality?

[Andreas Abel]

Hi Peter and Thorsten,

I agree that my justification is impredicative in spirit since it only 
works if you fix your domain of discourse before defining the semantics 
of types.  To make my definition work you need to commit to a term model 
(or something similar in spirit like a realisability model).

A purely predicative model does not need to fix a universe of values 
beforehand, but can construct the types and their inhabitants from 
scratch.

@Thorsten: where would you expect soundness problems?  Consistency, 
normalization, canonicity?

Cheers,
Andreas

On 12/21/10 11:19 AM, Peter Dybjer wrote:
> I agree with Thorsten that there is something impredicative about a definition like
>
> Id : (A : Set i) ->  A ->  A ->  Set
>
> If you think about Set i as the ith universe, (where i contrary to the Agda implementation is an external index) as inductively (or inductive-recursively) generated, with Id as an introduction rule, then Set = Set 0 is closed under something which is not yet defined (Set i, if i>  0).
>
> But maybe the intended meaning is something different?
>
> Peter
>
> On 20 Dec 2010, at 07:32, Andreas Abel wrote:
>
>> This is my view why we need to be skeptic:
>>
>> Indexing can be translated away using propositional equality.
>>
>> Propositional equality that just reflects the beta-equality of type theory can be justified regardless of levels, since you can define
>>
>>   Id : (A : Set i) ->  A ->  A ->  Set
>>   refl in Id A a a'<==>   a =beta a'
>
> I don't see how this is a justification in the sense that it shows that large equality is sound or conservative.
>
> Large equality certainly has an impredicative flavour. But it is not clear to me wether it extends the logical strength of the Type Theory.
>
> Thorsten
>
>> However, it is more difficult with beta-eta equality as we have in Agda.  There, equality is relative to type A.  This leads to a vicious cycle since Id A, living in Set 0, is prior to A in Set i, but the definition of Id A requires the definition of A.