From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.209.3 with SMTP id i3mr3248558wmg.7.1473169478059; Tue, 06 Sep 2016 06:44:38 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.17.7 with SMTP id 7ls1818668wmr.0.canary; Tue, 06 Sep 2016 06:44:37 -0700 (PDT) X-Received: by 10.28.168.149 with SMTP id r143mr2483182wme.1.1473169477219; Tue, 06 Sep 2016 06:44:37 -0700 (PDT) Return-Path: Received: from mail-lf0-x22e.google.com (mail-lf0-x22e.google.com. [2a00:1450:4010:c07::22e]) by gmr-mx.google.com with ESMTPS id w79si1221863wmw.0.2016.09.06.06.44.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 06 Sep 2016 06:44:37 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::22e as permitted sender) client-ip=2a00:1450:4010:c07::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::22e as permitted sender) smtp.mailfrom=andrew....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x22e.google.com with SMTP id g62so146332555lfe.3 for ; Tue, 06 Sep 2016 06:44:37 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=WY6QpZU6hXq3LmSj+pHwPp5NCqJvKBuSis9QCqcK2bA=; b=0d7Ly67tKBRE9bM4koV48ToRV/8ZXqSdKM6GbvbSgiAvb4/JrA8mfenzy9Jh/g+RsM gNNz70HdolF9Qau9lXDoPAz32eSBeO+3kEX4cD9ULfQ6+3gZXv7pRhCuImWQ7ke7wtLZ Ofvw1hAPJb+40xzO026e4PGH0U8taS+8qFgHx76h5JBPPsG3FXFjjzIWdZ5Ol1xgam4C +eSSt1tvEhw7FrYU/USEZm45JpYS4PTq6zKDFmtEfb8/Y5kzAiRDvu58XIhP2Ug17xi1 g/UolZNcEAD1FlG9MRx3Hlub1UUq0jf0EFMUzH+hJfPRulfm+Y1MuOtxiUtzPxZ04o1P GKdg== X-Gm-Message-State: AE9vXwNNyzEnXxGtf6QFaNiEBzxxUTjzJ7uV33HHQW8/qtX0EZep55DkH6wgYWFLS+YZJA4EiCuE/KfXoqOGyA== X-Received: by 10.25.16.101 with SMTP id f98mr5513117lfi.54.1473169476856; Tue, 06 Sep 2016 06:44:36 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.83.143 with HTTP; Tue, 6 Sep 2016 06:44:36 -0700 (PDT) In-Reply-To: References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> From: Andrew Polonsky Date: Tue, 6 Sep 2016 15:44:36 +0200 Message-ID: Subject: Re: [HoTT] A puzzle about "univalent equality" To: Peter LeFanu Lumsdaine Cc: Michael Shulman , Dan Licata , Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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=E2=80=99t* mean that Andews=E2=80= =99 original goal > =E2=80=9Cproj1 Y =3D tt=E2=80=9D is necesarily inhabited, if the funext w= itness used early in > his development is taken just from weak funext. > > The proof =E2=80=9Cweak funext implies strong funext=E2=80=9D shows that = given some witness > funext0 of weak funext (i.e. funext0 : (forall X Y f g, f =3D=3D g -> f = =3D g)), > then you can construct some new witness funext1, which additionally is a > (two-sided) inverse for the canonical map the other way (=E2=80=9Cap10=E2= =80=9D in the > current HoTT library). (I blogged the details here: > https://homotopytypetheory.org/2011/12/19/strong-funext-from-weak/) > > But it *doesn=E2=80=99t* show that the original witness funext0 is an inv= erse 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=E2=80=99s original goal =E2=80=9Cproj1 Y =3D tt=E2=80=9D depends o= n the witness used earlier > for funext =E2=80=94 so if that witness happens to conjugate paths Bool = =E2=80=93> Bool in > Type by the non-trivial auto-equivalence of Bool, then one could have pro= j1 > Y =3D ff. > > =E2=80=93p. > > >> >> 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 n= ot >> >> provable in "book HoTT=E2=80=9D. >> > >> > 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=3Dg -> f=3D=3Dg) is an equivale= nce, >> > 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > >