[Agda] Fin n -> Fin n extensional?

[Abhishek Anand]

Thanks Jason. Your argument is convincing. Already at the second line,  (\_ →
0) and (\_ → 1)  being definitionally equal contradicts my understanding of
Coq's definitional equality.
Are your assumptions valid in Agda with K?
In other words, is it true that in Agda with K, any proof of equality (Id)
of closed terms computes down to refl?


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

On Wed, Feb 18, 2015 at 12:06 PM, Jason Gross <jasongross9 at gmail.com> wrote:

> 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/20150219/0220c163/attachment.html