[Agda] Question about coinductive types

[Nils Anders Danielsson]

On 04/02/2019 13.42, Pierre Hyvernat wrote:
> The reason I ask is that writing out explicit bisimilarity proofs for
> general indexed containers in Agda is **very** painful.

I think that in Cubical Agda bisimilarity is equal to propositional
equality. Perhaps you could consider using that variant of Agda instead.

-- 
/NAD