[Agda] Fin n -> Fin n extensional?

[Aaron Stump]

Sorry, but what does "functions at type (Fin n -> Fin n) are 
extensional" mean?  I know what extensional equality is, and I am 
assuming this is some related terminology, but I am not sure precisely what.
Thanks,
Aaron
On 02/18/2015 09:47 AM, João Paulo Pizani Flor wrote:
> Not yet (couldn't find it anywhere), but I will probably need it for 
> my Ph.D project, so maybe it will come in some time...
>
> Cheers,
>
> João Pizani, M.Sc <j.p.pizaniflor at uu.nl <mailto:j.p.pizaniflor at uu.nl>>
> Promovendus - Departement Informatica
> Faculteit Bètawetenschappen - Universiteit Utrecht
>
> On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette <carette at mcmaster.ca 
> <mailto:carette at mcmaster.ca>> wrote:
>
>     Does anyone have a proof in Agda that functions at type (Fin n ->
>     Fin n) are extensional?
>     Jacques
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150218/8783f19d/attachment-0001.html