[Agda] Re: [Coq-Club] Re: Agda beats Coq

[Arnaud Spiwack]

As hour being late, I wasn't being as clear as I should. I meant that 
bisimilarity implies intentionnal equality *in Coq* (and so it does in 
Agda2 if I'm not mistaken). But this doesn't close the case. (as I was 
saying I personnally believe we shouldn't have this property).


Arnaud Spiwack

Arnaud Spiwack a écrit :
> As a matter of fact, the most natural bisimalirity on streams does 
> imply intentionnal equality. Which can be considered quite useful, but 
> I've got the feeling it's not a good idea. This is actually what makes 
> that Coq conversion is not decidable or Coq doesn't have subject 
> reduction (choose whichever you want). There are quite some 
> metaphysical issues here. ITT, ETT, OTT, whichever intermediate 
> alternative, Impredicative, Predicative, ... There is enough to fight 
> over all night long.
>
>
> Arnaud Spiwack
>
> Xavier Leroy a écrit :
>> Aaron Bohannon wrote:
>>
>>  
>>> [...] That is, may I safely assert that a standard definition of
>>> bisimilarity on a coinductive data type implies the default
>>> (intensional) equality ("=")?  (I don't know if this question is
>>> relevant to Agda.)
>>>     
>>
>> Thanks for raising this question, as I've been wondering about it for
>> a while.
>>
>> Let me take streams (infinite lists) as a concrete example of
>> coinductive datatype.  My (limited) understanding is that you could
>> make a set-theoretic model of streams where a stream of A is a
>> function nat -> A, so your property would amount to function
>> extensionality, which holds in this model.  However, I'm pretty sure
>> that if you assert function extensionality as an axiom in Coq, you
>> still cannot prove the extensionality property over streams stated
>> above...
>>
>> Expecting more informed replies from true logicians,
>>
>> - Xavier Leroy
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.futurs.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>           http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>>
>>   
>
>