[Agda] Size of propositional equality?

[Peter Dybjer]

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



________________________________________
From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Thorsten Altenkirch [txa at Cs.Nott.AC.UK]
Sent: Monday, December 20, 2010 7:58 PM
To: Andreas Abel
Cc: Nils Anders Danielsson; agda at lists.chalmers.se
Subject: Re: [Agda] Size of propositional equality?

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

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda