[Agda] Fin n -> Fin n extensional?

[Jason Gross]

Here's one, I think, for showing impossibility of inhabiting the type (f g
: Void → ℕ) → Id f g:
Assuming the type theory is strongly normalizing on terms of identity type,
the only closed proof of equality of two closed functions must be refl.
Thus, if (\_ → 0) and (\_ → 1) are equal, they must be definitionally equal
in a strongly normalizing type theory.  From (Id f g), we can obtain (x :
Void) → Id (f x) (g x); it's behavior is to send refl to refl.  Thus, when
we plug in refl : Id (\_ → 0) (\_ → 1), we get a proof of Void → Id 0 1
which reduces to \_ → refl.  But this is a contradiction, for refl does not
prove Id 0 1.

On Wed, Feb 18, 2015 at 11:37 AM, Abhishek Anand <
abhishek.anand.iitg at gmail.com> wrote:

> 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
>>
>>
>
> _______________________________________________
> 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/c0c56ee4/attachment-0001.html