[Agda] Size of propositional equality?

[Thorsten Altenkirch]

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.
> 
> Cheers,
> Andreas
> 
> On 12/17/10 7:40 PM, Nils Anders Danielsson wrote:
>> On 2010-12-17 16:11, Alan Jeffrey wrote:
>>> Is the skepticism a general one about sets being indexed by a set from
>>> a larger universe, or is it specific to propositional equality?
>> 
>> The former.
>> 
> 
> -- 
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda