[Agda] Question about coinductive types

[Pierre Hyvernat]

>Indeed, there is a proof that bisimilarity is (path-)equal to
>(path-)equality in our cubical library:
>
That's great!
Do you know if the case of streams generalizes to arbitrary "M-types", 
or even better, greatest fixed points of indexed containers, at least 
theoretically?

Or put in other words, is cubical type theory compatible with the 
property "bisimulation is equal to path-equality" for such general 
notion of coinductive types?


>However Cubical Agda does not yet properly support all the features of
>Agda, in particular inductive families are not yet supported. So
>depending on what you want to do it might or might not currently suit
>your needs.
>
At the moment, my code doesn't use any "modern" (read univalence and 
cubes) features and I prefer to keep it that way.
Some things might become possible, but probably not easy, nor 
interesting.
(Using cubes, and equality over equalities has been on my TODO list for 
some time though...)


Pierre
-- 
When a distinguished but elderly scientist states that
something is possible, he is almost certainly right.
When he states that something is impossible, he is very
probably wrong.
    -- Arthur C. Clarke