[Agda] Fin n -> Fin n extensional?
Dan Licata
drl at cs.cmu.edu
Wed Feb 18 17:20:07 CET 2015
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150218/c652c1d5/attachment.html
More information about the Agda
mailing list