<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;"><div>They should be neither – the identity type Id_A should have the same polarity as the type A.</div><div><br></div><div>Thorsten</div><div><br></div><span id="OLK_SRC_BODY_SECTION"><div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt"><span style="font-weight:bold">From: </span> Gabriel Scherer <<a href="mailto:gabriel.scherer@gmail.com">gabriel.scherer@gmail.com</a>><br><span style="font-weight:bold">Date: </span> Tue, 24 Feb 2015 08:59:35 +0000<br><span style="font-weight:bold">To: </span> Dan Doel <<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>><br><span style="font-weight:bold">Cc: </span> agda list <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br><span style="font-weight:bold">Subject: </span> Re: [Agda] Fin n -> Fin n extensional?<br></div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><div dir="ltr">In general my understanding of type theory is that, in natural deduction calculi (all typed lambda-calculi) negative types (functions and records-with-projections) are easy to eta-expand, and positives (sums) are hard. I'm not sure whether identity types can be given a polarity, but it certainly would not be negative : their introduction rule is not inversible.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 24, 2015 at 1:30 AM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@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 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"><span class="">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></span><div><div class="h5"><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><div><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" target="_blank">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" target="_blank">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" target="_blank">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" target="_blank">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" target="_blank">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" target="_blank">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" target="_blank">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" 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>
> >>>>><br>
> >>>>> _______________________________________________ Agda mailing<br>
> >>>>> list <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>
> >>>>><br>
> >>>>><br>
> >>>>> _______________________________________________ Agda mailing<br>
> >>>>> list <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>
> >>>>><br>
> >>>><br>
> >>>> _______________________________________________ Agda mailing<br>
> >>>> list <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>
> >>>><br>
> >>><br>
> >><br>
> >><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>
> > -----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" 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>
> 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>
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></div></div></blockquote></div></div></div><br></div><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></blockquote></div><br></div></blockquote></span><PRE>
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it.
Please do not use, copy or disclose the information contained in this
message or in any attachment. Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.
This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.
</PRE></body></html>