<div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">I imagine Agda doesn&#39;t do eta expansion of the identity type because it doesn&#39;t do eta expansion of any inductive type. It only does it for records and functions.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">If the identity type were a builtin, and all indexed types were expected to be defined by making reference to the identity type (or at least, were considered sugar for such), it would probably enable special treatment; it&#39;s probably how Epigram would have worked (they were considering other judgmental rewrites as well, like functor and monad axioms). Detecting which indexed inductive types are sufficiently identity-like to eta expand, or blessing only one (which I guess could be done since there are already pragmas informing Agda of the identity type for use in `rewrite`) would be difficult in the first case (probably) and weird in both.<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 23, 2015 at 3:05 PM, Jon Sterling <span dir="ltr">&lt;<a href="mailto:jon@jonmsterling.com" target="_blank">jon@jonmsterling.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Andrea,<br>
<br>
Out of curiosity, is the reason that Agda does not do eta expansion at<br>
the identity type because it would cause false identifications to become<br>
true judgementally in an open term?<br>
<br>
Kind regards,<br>
Jon<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
On Mon, Feb 23, 2015, at 10:50 AM, Andrea Vezzosi wrote:<br>
&gt; As a side note, Agda doesn&#39;t actually do any eta expansion at the Id<br>
&gt; type, e.g. two postulated equalities won&#39;t be judgementally equal.<br>
&gt;<br>
&gt; However without postulates (or primTrustMe) it is still the case that<br>
&gt; every proof of equality in a closed context will evaluate to refl.<br>
&gt; Axiom K actually computes away as soon as the proof becomes refl, so<br>
&gt; it&#39;s not making this any harder.<br>
&gt;<br>
&gt;<br>
&gt; Cheers,<br>
&gt; Andrea<br>
&gt;<br>
&gt; On Mon, Feb 23, 2015 at 4:38 PM, Neelakantan Krishnaswami<br>
&gt; &lt;<a href="mailto:n.krishnaswami@cs.bham.ac.uk">n.krishnaswami@cs.bham.ac.uk</a>&gt; wrote:<br>
&gt; &gt; -----BEGIN PGP SIGNED MESSAGE-----<br>
&gt; &gt; Hash: SHA1<br>
&gt; &gt;<br>
&gt; &gt; Hello,<br>
&gt; &gt;<br>
&gt; &gt; Definitional equality including Axiom K (uniqueness of identity proofs)<br>
&gt; &gt; remains decidable.<br>
&gt; &gt;<br>
&gt; &gt; The reason is that you can split the implementation of judgemental<br>
&gt; &gt; into two alternating phases -- weak-head normalization and<br>
&gt; &gt; type-directed eta-expansion. Just as with eta for unit, this means<br>
&gt; &gt; that when you compare terms at equality type, you can simply succeed.<br>
&gt; &gt;<br>
&gt; &gt; Concretely, if you have proofs p and q at type Id[X](e,e&#39;) such that<br>
&gt; &gt; p,q :  Id[X](e,e&#39;), then you can eta-expand to p ==&gt; refl and<br>
&gt; &gt; q ==&gt; refl, and then refl will be judged to be equal to itself.<br>
&gt; &gt;<br>
&gt; &gt; If you restrict &quot;computation&quot; to mean beta-reduction, then equality<br>
&gt; &gt; proofs do not all have to *reduce* to refl. However, they all can<br>
&gt; &gt; *eta-expand* to refl.<br>
&gt; &gt;<br>
&gt; &gt; IMO, a very good reference on this is Andreas Abel&#39;s habilitation<br>
&gt; &gt; thesis. If you&#39;re in a hurry, then his FOSSACS 2011 paper with Gabriel<br>
&gt; &gt; Scherer &quot;On Irrelevance and Algorithmic Equality in Predicative Type<br>
&gt; &gt; Theory&quot; was a relatively accessible introduction to this approach.<br>
&gt; &gt;<br>
&gt; &gt;<br>
&gt; &gt; Best,<br>
&gt; &gt; Neel<br>
&gt; &gt;<br>
&gt; &gt; On 19/02/15 20:54, Abhishek Anand wrote:<br>
&gt; &gt;&gt; Thanks Jason. Your argument is convincing. Already at the second<br>
&gt; &gt;&gt; line,  (\_ → 0) and (\_ → 1)  being definitionally equal<br>
&gt; &gt;&gt; contradicts my understanding of Coq&#39;s definitional equality. Are<br>
&gt; &gt;&gt; your assumptions valid in Agda with K? In other words, is it true<br>
&gt; &gt;&gt; that in Agda with K, any proof of equality (Id) of closed terms<br>
&gt; &gt;&gt; computes down to refl?<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; Thanks, -- Abhishek <a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a><br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; On Wed, Feb 18, 2015 at 12:06 PM, Jason Gross<br>
&gt; &gt;&gt; &lt;<a href="mailto:jasongross9@gmail.com">jasongross9@gmail.com</a>&gt; wrote:<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt;&gt; Here&#39;s one, I think, for showing impossibility of inhabiting the<br>
&gt; &gt;&gt;&gt; type (f g : Void → ℕ) → Id f g: Assuming the type theory is<br>
&gt; &gt;&gt;&gt; strongly normalizing on terms of identity type, the only closed<br>
&gt; &gt;&gt;&gt; proof of equality of two closed functions must be refl.  Thus, if<br>
&gt; &gt;&gt;&gt; (\_ → 0) and (\_ → 1) are equal, they must be definitionally<br>
&gt; &gt;&gt;&gt; equal in a strongly normalizing type theory.  From (Id f g), we<br>
&gt; &gt;&gt;&gt; can obtain (x : Void) → Id (f x) (g x); it&#39;s behavior is to send<br>
&gt; &gt;&gt;&gt; refl to refl.  Thus, when we plug in refl : Id (\_ → 0) (\_ → 1),<br>
&gt; &gt;&gt;&gt; we get a proof of Void → Id 0 1 which reduces to \_ → refl.  But<br>
&gt; &gt;&gt;&gt; this is a contradiction, for refl does not prove Id 0 1.<br>
&gt; &gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt; On Wed, Feb 18, 2015 at 11:37 AM, Abhishek Anand &lt;<br>
&gt; &gt;&gt;&gt; <a href="mailto:abhishek.anand.iitg@gmail.com">abhishek.anand.iitg@gmail.com</a>&gt; wrote:<br>
&gt; &gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt; Unprovability of void-ext has been known to be the reason why<br>
&gt; &gt;&gt;&gt;&gt; one cannot (in Coq) code up natural numbers as W Types.<br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt; Here is a quote : &quot;This is because one cannot prove that there<br>
&gt; &gt;&gt;&gt;&gt; is only a unique function from the empty set to the set of<br>
&gt; &gt;&gt;&gt;&gt; natural numbers without using extensional equality.&quot; from<br>
&gt; &gt;&gt;&gt;&gt; <a href="https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes" target="_blank">https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes</a><br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt; However, I don&#39;t know a formal (meta-theoretical) proof of<br>
&gt; &gt;&gt;&gt;&gt; unprovability of void-ext. I&#39;d be grateful if someone can point<br>
&gt; &gt;&gt;&gt;&gt; us to such a  proof.<br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt; -- Abhishek <a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a><br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt; On Wed, Feb 18, 2015 at 11:20 AM, Dan Licata &lt;<a href="mailto:drl@cs.cmu.edu">drl@cs.cmu.edu</a>&gt;<br>
&gt; &gt;&gt;&gt;&gt; wrote:<br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; Can you even do this (without otherwise assuming function<br>
&gt; &gt;&gt;&gt;&gt;&gt; extensionality)?<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; For example, for Fin 0, isn&#39;t it the same as saying &quot;any<br>
&gt; &gt;&gt;&gt;&gt;&gt; function from 0 to A is abort&quot;:<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; data Id {A : Set} (a : A) : A → Set where refl : Id a a<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; data Void : Set where<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; abort : {A : Set} → Void → A abort ()<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; void-ext : {A : Set} → (f : Void → A) → Id f abort void-ext f<br>
&gt; &gt;&gt;&gt;&gt;&gt; = {!!}<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; (void-ext is sufficient; is it necessary?) and if so, can you<br>
&gt; &gt;&gt;&gt;&gt;&gt; prove that?  I don&#39;t see how off the top of my head.<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; -Dan<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; On Feb 18, 2015, at 10:47 AM, João Paulo Pizani Flor &lt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; <a href="mailto:J.P.PizaniFlor@uu.nl">J.P.PizaniFlor@uu.nl</a>&gt; wrote:<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; Not yet (couldn&#39;t find it anywhere), but I will probably need<br>
&gt; &gt;&gt;&gt;&gt;&gt; it for my Ph.D project, so maybe it will come in some<br>
&gt; &gt;&gt;&gt;&gt;&gt; time...<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; Cheers,<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; João Pizani, M.Sc &lt;<a href="mailto:j.p.pizaniflor@uu.nl">j.p.pizaniflor@uu.nl</a>&gt; Promovendus -<br>
&gt; &gt;&gt;&gt;&gt;&gt; Departement Informatica Faculteit Bètawetenschappen -<br>
&gt; &gt;&gt;&gt;&gt;&gt; Universiteit Utrecht<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette<br>
&gt; &gt;&gt;&gt;&gt;&gt; &lt;<a href="mailto:carette@mcmaster.ca">carette@mcmaster.ca</a>&gt; wrote:<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt;&gt; Does anyone have a proof in Agda that functions at type<br>
&gt; &gt;&gt;&gt;&gt;&gt;&gt; (Fin n -&gt; Fin n) are extensional? Jacques<br>
&gt; &gt;&gt;&gt;&gt;&gt;&gt; _______________________________________________ Agda<br>
&gt; &gt;&gt;&gt;&gt;&gt;&gt; mailing list <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt;&gt;&gt;&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt; &gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; _______________________________________________ Agda mailing<br>
&gt; &gt;&gt;&gt;&gt;&gt; list <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt;&gt;&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt; _______________________________________________ Agda mailing<br>
&gt; &gt;&gt;&gt;&gt;&gt; list <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt;&gt;&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt; _______________________________________________ Agda mailing<br>
&gt; &gt;&gt;&gt;&gt; list <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt;&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;&gt;<br>
&gt; &gt;&gt;&gt;<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt;<br>
&gt; &gt;&gt; _______________________________________________ Agda mailing list<br>
&gt; &gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt; &gt;&gt;<br>
&gt; &gt; -----BEGIN PGP SIGNATURE-----<br>
&gt; &gt; Version: GnuPG v2.0.14 (GNU/Linux)<br>
&gt; &gt;<br>
&gt; &gt; iQIbBAEBAgAGBQJU60laAAoJEFHmop5RZGmSfJcP91HMj9P8+iiF344OtyF+Pfv1<br>
&gt; &gt; IUk+w4IndUMQcDPFys0GCX9VyMeg5W3ezwV1eYYLNlSghtR/rWAVtKRlDH/PQ8Hp<br>
&gt; &gt; Q9RJhpEo3gNMW1cBSHWTM7HpmcI2z8ttualtE/1+yK4XPRC0vXw6V6mOHv4KmDES<br>
&gt; &gt; xjhsKy4ut8Ah4pTXvb0+MkTvI46F7dpBlkpQmAFygpfOtNz7ahZ4+bQjlmdPMu6B<br>
&gt; &gt; DG9jwtA9HuEBoxR84Fni0w9gA5da+Ew7cF0mcuG777RK3M6NnuB+jnyk18w7qUKv<br>
&gt; &gt; bQ9s4Is0YZ4KHkDmNe6tVnTbDaivzQfN6rBTFPfrRPHCo0b4cU3Dpos7dQdOf56a<br>
&gt; &gt; qvlmC8hoB60KGaLYx+SqjAHfEudHsTPzpDQUHZE0T+zlqLBI1g8y9my20rd5PN3t<br>
&gt; &gt; S4sapKOVsVibd+XnNbGDhoRDA4Uy1KccO0O9Yt8w1/yTpJqik4DfB8g7tEIzsgc+<br>
&gt; &gt; 137F+WnUfNiilpukOWrhzSRmxpmOgGZaA96o4tsq6eZjf8w9OSZeYFzEqn+pCtci<br>
&gt; &gt; gClqrFGIdbBXHEcOMnJ5K+Y1y+1himsvfM8XavdE0tTfv2+aGknpwm9qRs6SG7+w<br>
&gt; &gt; gNV18wNhkL6BqdDTnEIJ6y1PvK/IDmi6D9Ar9eL8nvcELzzsEbDFLFWkm/ElSzZ6<br>
&gt; &gt; OC285Dst5uKeClsp238=<br>
&gt; &gt; =qT5j<br>
&gt; &gt; -----END PGP SIGNATURE-----<br>
&gt; &gt; _______________________________________________<br>
&gt; &gt; Agda mailing list<br>
&gt; &gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; &gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">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>
</div></div></blockquote></div><br></div>