From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.66.14.166 with SMTP id q6mr13169174pac.48.1473166638395; Tue, 06 Sep 2016 05:57:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.43.24 with SMTP id o24ls4566376otb.35.gmail; Tue, 06 Sep 2016 05:57:17 -0700 (PDT) X-Received: by 10.157.52.147 with SMTP id g19mr7913800otc.30.1473166637849; Tue, 06 Sep 2016 05:57:17 -0700 (PDT) Return-Path: Received: from mail-ua0-x22e.google.com (mail-ua0-x22e.google.com. [2607:f8b0:400c:c08::22e]) by gmr-mx.google.com with ESMTPS id v141si2152195vke.1.2016.09.06.05.57.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 06 Sep 2016 05:57:17 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22e as permitted sender) client-ip=2607:f8b0:400c:c08::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22e as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-ua0-x22e.google.com with SMTP id 31so47628464uao.0 for ; Tue, 06 Sep 2016 05:57:17 -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; bh=pqG2ecrSRSttC02rIaiNglKjeCwktUvCYOcRCbBED3k=; b=YIplABhwIQOSwYahYMCtGDPUvKe7BL46Ng5UPB3fv9hkum/CmyAbuLwzvqNeXUh0HA gPoTXsoF97agtqmJMEz5EPXRDM2xZIBY8k+5aCXiuwNfg1+p/XZWZU1dNUI3zDF0qO75 q4pgeY7fYrGbK8zd6wxXHNPUvAIV2u0vIIPqSqXnfpndIh3ZbILI4q4em7MmZBFb6E2r HqMGHOPnQ5ze8HJr3TIApEUjcR7IT2hD2dDmHSwwi6t+aZ8On0OxhPeb8FpDY0QZhAle Qu19rblM5uaOMdw7/Sz/zGTCL7Thsm0dAjMEs4dF1EjhQuv5nk8vS5+V9s0gqtHdt40g t4cg== X-Gm-Message-State: AE9vXwME6v9IBjadUPsqFUOIUM1D1asTSvVACiKvi3z4RD5mhVxvFzQW6Kt+kZC6d6nU5hvc1bMdK2gryML0WA== X-Received: by 10.159.39.97 with SMTP id a88mr24719006uaa.77.1473166637660; Tue, 06 Sep 2016 05:57:17 -0700 (PDT) MIME-Version: 1.0 Received: by 10.159.33.246 with HTTP; Tue, 6 Sep 2016 05:57:16 -0700 (PDT) In-Reply-To: References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> From: Peter LeFanu Lumsdaine Date: Tue, 6 Sep 2016 14:57:16 +0200 Message-ID: Subject: Re: [HoTT] A puzzle about "univalent equality" To: Michael Shulman Cc: Andrew Polonsky , Dan Licata , Homotopy Type Theory Content-Type: multipart/alternative; boundary=94eb2c122d0c220017053bd65661 --94eb2c122d0c220017053bd65661 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 wit= ness 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 gi= ven 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 inver= se 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 on = 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 proj1 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 no= t > 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 equivalen= ce, > > 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. > --94eb2c122d0c220017053bd65661 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On T= ue, Sep 6, 2016 at 2:32 PM, Michael Shulman <shu...@sandiego.edu&g= t; wrote:
Altho= ugh, as Voevodsky showed, weak funext implies strong funext.

Just to clarify, though, this *doesn=E2=80=99t* =C2=A0mea= n that Andews=E2=80=99 original goal =E2=80=9Cproj1 Y =3D tt=E2=80=9D is ne= cesarily inhabited, if the funext witness used early in his development is = taken just from weak funext.

The proof =E2=80=9Cwe= ak funext implies strong funext=E2=80=9D shows that given some witness fune= xt0 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). =C2=A0(I blogged the details here:= =C2=A0https://homotopytypetheory.org/2011/12/19/strong-funext-from-weak= /)

But it *doesn=E2=80=99t* show that the orig= inal 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-tri= vial loops in the codomain type.=C2=A0 Andrew=E2=80=99s original goal =E2= =80=9Cproj1 Y =3D tt=E2=80=9D depends on the witness used earlier for funex= t =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 proj1 Y =3D ff.

=E2=80=93p.

=C2=A0
<= div class=3D"gmail-HOEnZb">
On Tue, Sep 6, 2016 at 12:30 AM, Andrew Polonsky
<andrew....@gmail.com> wr= ote:
> Thanks, Mike and Dan.=C2=A0 And congratulations on giving essentially<= br> > identical solutions at essentially identical times, in two different > languages!
>
>> I would be very surprised if there was something like this that wa= s not provable in "book HoTT=E2=80=9D.
>
> I believe there can't be, either.=C2=A0 But maybe this "belie= f" 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 th= e stronger
> formulation, that the canonical map (f=3Dg -> f=3D=3Dg) is an equiv= alence,
> to make the transports compute.
>
> Cheers,
> Andrew
>
> --
> You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send= an email to Homoto= pyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.google.com/d/opto= ut.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--94eb2c122d0c220017053bd65661--