[Agda] Propositional equality for coinductive records

Jannis Limperg jannis at limperg.de
Thu Feb 23 17:04:25 CET 2017


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


More information about the Agda mailing list