<div dir="ltr"><div>You can look at the cubical branch and the cubical demos.<br><br><a href="https://github.com/Saizan/cubical-demo/blob/master/Stream.agda#L45">https://github.com/Saizan/cubical-demo/blob/master/Stream.agda#L45</a><br><br></div>You can turn a bisimulation into an equality.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 23, 2017 at 5:32 PM, Jannis Limperg <span dir="ltr"><<a href="mailto:jannis@limperg.de" target="_blank">jannis@limperg.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear all,<br>
<br>
propositional equality for coinductive records is currently extremely<br>
restricted since it is not possible (as far as I can tell) to go from<br>
propositional equality of all fields to equality of the records. For<br>
example, it is impossible to define `R-ext` in the following example due<br>
to the inability to destruct `r` and `s`.<br>
<br>
<br>
    data ⊤ : Set where tt : ⊤<br>
<br>
    data _≡_ {a} {A : Set a} (x : A) : A → Set a where<br>
      refl : x ≡ x<br>
<br>
    record R : Set where<br>
      coinductive<br>
      field force : R<br>
<br>
    open R<br>
<br>
    R-ext : {r s : R} → force r ≡ force s → r ≡ s<br>
    R-ext = ?<br>
<br>
This contrasts with Coq (and probably Agda's old coinduction) which<br>
would allow similar equalities to be exploited.<br>
<br>
Now, propositional equality on coinductive data is not often useful<br>
anyway since it is too restrictive for most purposes. However, I have a<br>
corecursive function, say `f`, for which I can prove `force (f x) ≡<br>
force (g x)` for some simpler `g`, and being able to turn this into<br>
`f x ≡ g x` would make it much easier to apply the equation in other<br>
proofs. Reformulating it in terms of a bisimulation (`force r ≡ force s<br>
→ Bisim r s`) would be possible, but much less convenient for users of `f`.<br>
<br>
So,<br>
<br>
- Has anyone else experienced this problem (and perhaps found a good<br>
workaround)?<br>
- Would it be desirable to recover this form of 'extensionality' for<br>
coinductive records, and if so how could this be done?<br>
- Is adding `R-ext` as an axiom dangerous?<br>
<br>
Thanks for your consideration,<br>
Jannis<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>