[Agda] Propositional equality for coinductive records

[Jannis Limperg]

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