[Agda] Fin n -> Fin n extensional?

[Aaron Stump]

No wait, I spoke too soon.  That type says that for any n, for any 
functions f and g, and for any input x, if f x equals g x then f equals 
g.  That seems very strong.  It is saying if the functions have the same 
output on any particular input x, then they are equal.  I would have 
thought you meant:

fin-ext : (n : ℕ)(f g : Fin n → Fin n) → ((x : Fin n) → f x ≡ g x) → f ≡ g

Is that right?

Aaron

On 02/18/2015 10:04 AM, Andrés Sicard-Ramírez wrote:
> On 18 February 2015 at 10:51, Aaron Stump <aaron-stump at uiowa.edu> wrote:
>> Sorry, but what does "functions at type (Fin n -> Fin n) are extensional"
>> mean?
> fin-ext : (n : ℕ)(f g : Fin n → Fin n)(x : Fin n) → f x ≡ g x → f ≡ g
>
>