[Agda] Fin n -> Fin n extensional?

[Jason Gross]

On Thu, Feb 19, 2015 at 3:54 PM, Abhishek Anand <
abhishek.anand.iitg at gmail.com> wrote:

> In other words, is it true that in Agda with K, any proof of equality (Id)
> of closed terms computes down to refl?


I don't know what the conditions are for Agda's type theory to be strongly
normalizing on Id types.  I suspect it still holds with K, but I haven't
looked at any details.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150219/5a0d6ce0/attachment-0001.html