[Agda] Question about coinductive types

[Anders Mortberg]

Indeed, there is a proof that bisimilarity is (path-)equal to
(path-)equality in our cubical library:

https://github.com/agda/cubical/blob/master/Cubical/Codata/Stream/Properties.agda#L82

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.

--
Anders

On Mon, Feb 4, 2019 at 9:34 AM Nils Anders Danielsson <nad at cse.gu.se> wrote:
>
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda