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