[Agda] Fin n -> Fin n extensional?

[Jacques Carette]

Actually the reason for asking the original question was an attempt to 
prove the *equivalence* of these representations [including the full 
semiring structure on both sides].

Using Setoids to parametrize the concept of equivalence properly, our 
proof is 99% done.

Jacques

On 15-02-23 03:13 PM, Thorsten Altenkirch wrote:
> As discussed it is not. However, there is an alternative representation of
> (Fin n -> Fin m) which is extensional, namely "Vec (Fin m) n². It is not
> hard to define
>
> 	lam : (Fin n -> Fin m) -> Vec (Fin m) n
> 	app : Vec (Fin m) n -> Fin n -> Fin m
>
> but this is only a retract. However, we can prove
>
> 	(f g : Vec (Fin m) n) -> ((i : Fin n) -> app f i == app g i) -> f == g
>
> Thorsten
>
> On 18/02/2015 14:25, "Jacques Carette" <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
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda