[Agda] Propositional equality for coinductive records

[Andrea Vezzosi]

It should be consistent to postulate R-ext, similarly to how it's
consistent to postulate function extensionality.

On Thu, Feb 23, 2017 at 5:04 PM, Jannis Limperg <jannis at limperg.de> wrote:
> Interesting; I'll definitely take a closer look. In the mid-term, I'm
> hopeful that HoTT/cubical TT will render this issue obsolete.
> Short-term, I unfortunately can't rely on something this bleeding-edge
> (and I'd have to explain cubical type theory in the associated thesis,
> which is a little out of my league).
>
> Cheers,
> Jannis
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda