<div dir="ltr">Thanks Jason. Your argument is convincing. Already at the second line, <span style="font-size:13px">(\_ </span><span style="font-size:12.8000001907349px">→ 0) and (\_ → 1) being definitionally equal contradicts my </span>understanding<span style="font-size:12.8000001907349px"> of Coq's </span>definitional<span style="font-size:12.8000001907349px"> equality.</span><br><div>Are your assumptions valid in Agda with K?</div><div>In other words, is it true that in Agda with K, any proof of equality (Id) of closed terms computes down to refl?</div><div><br></div><div class="gmail_extra"><br></div><div class="gmail_extra">Thanks,<br clear="all"><div><div class="gmail_signature"><div>-- Abhishek</div><a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a></div></div>
<br><div class="gmail_quote">On Wed, Feb 18, 2015 at 12:06 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Here's one, I think, for showing impossibility of inhabiting the type <span style="font-size:12.8000001907349px">(f g : </span><span style="font-size:12.8000001907349px">Void</span><span style="font-size:12.8000001907349px"> </span><span style="font-size:12.8000001907349px">→ </span><span style="font-size:12.8000001907349px">ℕ</span><span style="font-size:12.8000001907349px">) → Id f g:</span></div><div>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 (\_ <span style="font-size:12.8000001907349px">→ 0) and (\_ </span><span style="font-size:12.8000001907349px">→ 1) are equal, they must be definitionally equal in a strongly normalizing type theory. From (Id f g), we can obtain (x : Void) </span><span style="font-size:12.8000001907349px">→ Id (f x) (g x); it's behavior is to send refl to refl. Thus, when we plug in refl : Id (\_ </span><span style="font-size:12.8000001907349px">→ 0) (\_ </span><span style="font-size:12.8000001907349px">→ 1), we get a proof of Void → Id 0 1 which reduces to \_ </span><span style="font-size:12.8000001907349px">→ refl. But this is a contradiction, for refl does not prove Id 0 1.</span></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 18, 2015 at 11:37 AM, Abhishek Anand <span dir="ltr"><<a href="mailto:abhishek.anand.iitg@gmail.com" target="_blank">abhishek.anand.iitg@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Unprovability of void-ext has been known to be the reason why one cannot (in Coq) <div>code up natural numbers as W Types.</div><div><br></div><div>Here is a quote :</div><div><div>"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."</div><div>from</div></div><div><div><a href="https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes" target="_blank">https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes</a><br></div><div><br></div><div>However, I don't know a formal (meta-theoretical) proof of unprovability of void-ext.</div><div>I'd be grateful if someone can point us to such a proof.</div></div><div><br></div></div><div class="gmail_extra"><br clear="all"><div><div><div>-- Abhishek</div><a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a></div></div><div><div>
<br><div class="gmail_quote">On Wed, Feb 18, 2015 at 11:20 AM, Dan Licata <span dir="ltr"><<a href="mailto:drl@cs.cmu.edu" target="_blank">drl@cs.cmu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">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> data Id {A : Set} (a : A) : A → Set where</div><div> refl : Id a a</div><div><br></div><div> data Void : Set where</div><div><br></div><div> abort : {A : Set} → Void → A</div><div> abort ()</div><div><br></div><div> void-ext : {A : Set} → (f : Void → A) → Id f abort</div><div> 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? I don't see how off the top of my head. </div><span><font color="#888888"><div><br></div><div>-Dan</div></font></span><div><div><div><br><div><div>On Feb 18, 2015, at 10:47 AM, João Paulo Pizani Flor <<a href="mailto:J.P.PizaniFlor@uu.nl" target="_blank">J.P.PizaniFlor@uu.nl</a>> wrote:</div><br><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><div dir="ltr"><div><div>João Pizani, M.Sc <<a href="mailto:j.p.pizaniflor@uu.nl" target="_blank">j.p.pizaniflor@uu.nl</a>><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"><<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>></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 -> 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" target="_blank">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br></blockquote></div><br></div></div></div></div><br>_______________________________________________<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/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div></div></div>
<br>_______________________________________________<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/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</div></div></blockquote></div><br></div></div>