[Agda] Question about coinductive types

[Andrea Vezzosi]

On Wed, Feb 6, 2019 at 10:26 AM Pierre Hyvernat
<pierre.hyvernat at univ-smb.fr> wrote:
>
>
> >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?

It should. We can prove that indexed M types are the final coalgebra
of an indexed container [1], so every expected property regarding the
equality type should follow.

[1] https://github.com/agda/cubical/blob/47254df222b04f8100c34518eaf56a88210de0d3/Cubical/Codata/M.agda

Cheers,
Andrea

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda