The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

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