[Agda] Propositional equality for coinductive records

[Apostolis Xekoukoulotakis]

You can look at the cubical branch and the cubical demos.

https://github.com/Saizan/cubical-demo/blob/master/Stream.agda#L45

You can turn a bisimulation into an equality.

On Thu, Feb 23, 2017 at 5:32 PM, Jannis Limperg <jannis at limperg.de> wrote:

> Dear all,
>
> propositional equality for coinductive records is currently extremely
> restricted since it is not possible (as far as I can tell) to go from
> propositional equality of all fields to equality of the records. For
> example, it is impossible to define `R-ext` in the following example due
> to the inability to destruct `r` and `s`.
>
>
>     data ⊤ : Set where tt : ⊤
>
>     data _≡_ {a} {A : Set a} (x : A) : A → Set a where
>       refl : x ≡ x
>
>     record R : Set where
>       coinductive
>       field force : R
>
>     open R
>
>     R-ext : {r s : R} → force r ≡ force s → r ≡ s
>     R-ext = ?
>
> This contrasts with Coq (and probably Agda's old coinduction) which
> would allow similar equalities to be exploited.
>
> Now, propositional equality on coinductive data is not often useful
> anyway since it is too restrictive for most purposes. However, I have a
> corecursive function, say `f`, for which I can prove `force (f x) ≡
> force (g x)` for some simpler `g`, and being able to turn this into
> `f x ≡ g x` would make it much easier to apply the equation in other
> proofs. Reformulating it in terms of a bisimulation (`force r ≡ force s
> → Bisim r s`) would be possible, but much less convenient for users of `f`.
>
> So,
>
> - Has anyone else experienced this problem (and perhaps found a good
> workaround)?
> - Would it be desirable to recover this form of 'extensionality' for
> coinductive records, and if so how could this be done?
> - Is adding `R-ext` as an axiom dangerous?
>
> Thanks for your consideration,
> Jannis
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170223/e31e1055/attachment.html>