<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Can you even do this (without otherwise assuming function extensionality)?<div><br></div><div>For example, for Fin 0, isn't it the same as saying "any function from 0 to A is abort":</div><div><br></div><div><div>&nbsp; data Id {A : Set} (a : A) : A → Set where</div><div>&nbsp; &nbsp; refl : Id a a</div><div><br></div><div>&nbsp; data Void : Set where</div><div><br></div><div>&nbsp; abort : {A : Set} → Void → A</div><div>&nbsp; abort ()</div><div><br></div><div>&nbsp; void-ext : {A : Set} → (f : Void → A) → Id f abort</div><div>&nbsp; void-ext f = {!!}</div></div><div><br></div><div>(void-ext is sufficient; is it necessary?)</div><div>and if so, can you prove that? &nbsp;I don't see how off the top of my head. &nbsp;</div><div><br></div><div>-Dan</div><div><br><div><div>On Feb 18, 2015, at 10:47 AM, João Paulo Pizani Flor &lt;<a href="mailto:J.P.PizaniFlor@uu.nl">J.P.PizaniFlor@uu.nl</a>&gt; wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr"><div>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...<br><br></div>Cheers,<br><div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div>João Pizani, M.Sc &lt;<a href="mailto:j.p.pizaniflor@uu.nl" target="_blank">j.p.pizaniflor@uu.nl</a>&gt;<br></div>Promovendus - Departement Informatica<br></div>Faculteit Bètawetenschappen - Universiteit Utrecht<br></div></div></div>
<br><div class="gmail_quote">On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette <span dir="ltr">&lt;<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Does anyone have a proof in Agda that functions at type (Fin n -&gt; Fin n) are extensional?<br>
Jacques<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div><br></div></div></div>
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></blockquote></div><br></div></body></html>