The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

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
> >
> >