[Agda] Re: Fin n -> Fin n extensional?

Stefan Monnier monnier at iro.umontreal.ca
Tue Feb 24 23:15:02 CET 2015


> The literature is full of work which erroneously conflates irrelevance in
> typechecking with irrelevance in execution.

IIUC, the key reason for the difference is that evaluation always
proceeds in the empty context, right?


        Stefan



More information about the Agda mailing list