[Agda] Fin n -> Fin n extensional?

[Abhishek Anand]

Unprovability of void-ext has been known to be the reason why one cannot
(in Coq)
code up natural numbers as W Types.

Here is a quote :
"This is because one cannot prove that there is only a unique function from
the empty set to the set of natural numbers without using extensional
equality."
from
https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes

However, I don't know a formal (meta-theoretical) proof of unprovability of
void-ext.
I'd be grateful if someone can point us to such a  proof.


-- Abhishek
http://www.cs.cornell.edu/~aa755/

On Wed, Feb 18, 2015 at 11:20 AM, Dan Licata <drl at cs.cmu.edu> wrote:

> Can you even do this (without otherwise assuming function extensionality)?
>
> For example, for Fin 0, isn't it the same as saying "any function from 0
> to A is abort":
>
>   data Id {A : Set} (a : A) : A → Set where
>     refl : Id a a
>
>   data Void : Set where
>
>   abort : {A : Set} → Void → A
>   abort ()
>
>   void-ext : {A : Set} → (f : Void → A) → Id f abort
>   void-ext f = {!!}
>
> (void-ext is sufficient; is it necessary?)
> and if so, can you prove that?  I don't see how off the top of my head.
>
> -Dan
>
> On Feb 18, 2015, at 10:47 AM, João Paulo Pizani Flor <J.P.PizaniFlor at uu.nl>
> 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>
> Promovendus - Departement Informatica
> Faculteit Bètawetenschappen - Universiteit Utrecht
>
> On Wed, Feb 18, 2015 at 3:25 PM, 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
>>
>
> _______________________________________________
> Agda mailing list
> 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/c888f21f/attachment.html