# Is extensionality for coinductive datatypes consistent with Coq's logic?

Given a coinductive datatype, one can usually (always?) define a bisimulation as the largest equivalence relation over it. I would like to add an axiom stating that if two members of the type are related by the bisimulation, they are equal in the sense of Leibniz equality (=). Would this make the logic inconsistent?

An example for streams:

CoInductive Stream A :=
| Cons : A -> Stream A -> Stream A.

CoInductive Stream_bisim A : Stream A -> Stream A -> Prop :=
| Stream_bisim_Cons :
forall x xs ys,
Stream_bisim A xs ys ->
Stream_bisim A (Cons A x xs) (Cons A x ys).

Axiom Stream_bisim_eq :
forall A xs ys,
Stream_bisim A xs ys ->
xs = ys.


My intuition is that this should be safe by analogy with functional extensionality, since it should not be possible to distinguish bisimilar streams by observation. But of course I'd prefer an actual proof (or at least expert testimony) to such informalities.

• One year later; did you manage to find the answer? – paulotorrens Nov 28 '17 at 15:47
• @paulotorrens No -- I still believe that this is safe, but still don't know for certain. In practice, Coq's generalised rewriting makes using bisim instead of propositional equality bearable, so I would tend not to use the axiom. – Jannis Limperg Nov 28 '17 at 20:11
• The last paragraph of section 2.2.2 of Simon Boulier's PhD thesis "Extending type theory with syntactic models" (tel.archives-ouvertes.fr/tel-02007839) states that it is provable in a univalent setting, if you use a well-chosen definition of stream, and gives references. – xavierm02 Dec 10 '19 at 12:53