From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.9.88 with SMTP id 85mr2380657ljj.0.1473200064868; Tue, 06 Sep 2016 15:14:24 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.207.17 with SMTP id f17ls710695lfg.31.gmail; Tue, 06 Sep 2016 15:14:23 -0700 (PDT) X-Received: by 10.46.9.88 with SMTP id 85mr2380654ljj.0.1473200063858; Tue, 06 Sep 2016 15:14:23 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id e21si83069wmc.2.2016.09.06.15.14.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 06 Sep 2016 15:14:23 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.127] (helo=bham.ac.uk) by sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1bhOdL-0007AU-OQ for HomotopyT...@googlegroups.com; Tue, 06 Sep 2016 23:14:23 +0100 Received: from host86-137-209-253.range86-137.btcentralplus.com ([86.137.209.253] helo=[192.168.1.112]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1bhOdL-0005cG-EW for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Tue, 06 Sep 2016 23:14:23 +0100 Subject: Re: [HoTT] A puzzle about "univalent equality" References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> To: Homotopy Type Theory From: Martin Escardo Message-ID: <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com> Date: Tue, 6 Sep 2016 23:14:22 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) I've been asking myself a similar question for some time now, and perhaps it is the time to share it, although I was waiting to have a more precise formulation, which I still don't. (So fill free to improve my question or to say why it can't be answered.) The nature of the type Id U X Y, in MLTT, is under-specified by the (intensional) MLTT "axioms". Maybe isProp(Id U X Y). This is the K-axiom (for the universe U). Maybe Id U X Y is canonically equivalent to the type X~Y of equivalences. This is the univalence axiom (for the universe U). Maybe ... many more interesting things are possible? What else is consistent beyond K and univalence, and possibly interesting? Some people like the K-axiom for U because ... (let them fill the answer). We like the univalence axiom for U because, "magically", it makes Id behave as we think equality should behave (equality of groups should be group isomorphism, for instance, and it is, under univalence). But ... can we avoid the magical aspect? Can we stare at the type (Id U X Y) objectively, mathematically, say within intensional MLTT, where it was introduced, and, internally in MLTT, ponder what it can be, and identify the only "compelling" thing it can be as the type of equivalences X~Y, where "compelling" is a notion remote from univalence? At the moment, univalence is "experimentally" interesting/compelling: it gives function extensionality, it gives propositional extensionality, it gives that the fundamental group of the circle HIT is Z, it gives that equality of categories is categorical equivalence, and much more. But can we "ultimately" justify it as the "intrinsically mathematically appealing" determination of Id U X Y, before we consider the interesting experimental consequences? Martin On 06/09/16 14:44, Andrew Polonsky wrote: > These are all good points. I now have an exhaustive answer to my > motivating question. > > Thanks, > Andrew > > On Tue, Sep 6, 2016 at 2:57 PM, Peter LeFanu Lumsdaine > wrote: >> On Tue, Sep 6, 2016 at 2:32 PM, Michael Shulman >> wrote: >>> >>> Although, as Voevodsky showed, weak funext implies strong funext. >> >> >> Just to clarify, though, this *doesn’t* mean that Andews’ original goal >> “proj1 Y = tt” is necesarily inhabited, if the funext witness used early in >> his development is taken just from weak funext. >> >> The proof “weak funext implies strong funext” shows that given some witness >> funext0 of weak funext (i.e. funext0 : (forall X Y f g, f == g -> f = g)), >> then you can construct some new witness funext1, which additionally is a >> (two-sided) inverse for the canonical map the other way (“ap10” in the >> current HoTT library). (I blogged the details here: >> https://homotopytypetheory.org/2011/12/19/strong-funext-from-weak/) >> >> But it *doesn’t* show that the original witness funext0 is an inverse for >> ap10, and indeed the proof points to how this may fail: funext0 might >> conjugate paths by some family of non-trivial loops in the codomain type. >> Andrew’s original goal “proj1 Y = tt” depends on the witness used earlier >> for funext — so if that witness happens to conjugate paths Bool –> Bool in >> Type by the non-trivial auto-equivalence of Bool, then one could have proj1 >> Y = ff. >> >> –p. >> >> >>> >>> On Tue, Sep 6, 2016 at 12:30 AM, Andrew Polonsky >>> wrote: >>>> Thanks, Mike and Dan. And congratulations on giving essentially >>>> identical solutions at essentially identical times, in two different >>>> languages! >>>> >>>>> I would be very surprised if there was something like this that was not >>>>> provable in "book HoTT”. >>>> >>>> I believe there can't be, either. But maybe this "belief" is really a >>>> matter of definition, in that the equalities which are "supposed to" >>>> hold, are precisely those which can be derived in book HoTT. >>>> >>>> What I find subtle in the above example is that it apparently cannot >>>> be done with the "pre-HoTT" FunExt axiom; you need to use the stronger >>>> formulation, that the canonical map (f=g -> f==g) is an equivalence, >>>> to make the transports compute. >>>> >>>> Cheers, >>>> Andrew >>>> >>>> -- >>>> You received this message because you are subscribed to the Google >>>> Groups "Homotopy Type Theory" group. >>>> To unsubscribe from this group and stop receiving emails from it, send >>>> an email to HomotopyTypeThe...@googlegroups.com. >>>> For more options, visit https://groups.google.com/d/optout. >>> >>> -- >>> You received this message because you are subscribed to the Google Groups >>> "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, send an >>> email to HomotopyTypeThe...@googlegroups.com. >>> For more options, visit https://groups.google.com/d/optout. >> >> >