[Agda] Size of propositional equality?

[Andreas Abel]

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'

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/