From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.66.231.2 with SMTP id tc2mr28513346pac.45.1473166572589; Tue, 06 Sep 2016 05:56:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.22.133 with SMTP id c5ls1754072ote.48.gmail; Tue, 06 Sep 2016 05:56:11 -0700 (PDT) X-Received: by 10.200.52.230 with SMTP id x35mr10648576qtb.23.1473166571934; Tue, 06 Sep 2016 05:56:11 -0700 (PDT) Return-Path: Received: from smtp01.srv.cs.cmu.edu (smtp01.srv.cs.cmu.edu. [128.2.217.200]) by gmr-mx.google.com with ESMTPS id l185si1857190ywb.5.2016.09.06.05.56.11 for (version=TLS1 cipher=AES128-SHA bits=128/128); Tue, 06 Sep 2016 05:56:11 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of d...@cs.cmu.edu designates 128.2.217.200 as permitted sender) client-ip=128.2.217.200; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of d...@cs.cmu.edu designates 128.2.217.200 as permitted sender) smtp.mailfrom=d...@cs.cmu.edu; dmarc=fail (p=NONE dis=NONE) header.from=cmu.edu Received-SPF: none (cs.cmu.edu: No applicable sender policy available) receiver=smtp01.srv.cs.cmu.edu; identity=mailfrom; envelope-from="d...@cs.cmu.edu"; helo="[192.168.144.101]"; client-ip=73.142.151.116 Received: from [192.168.144.101] (c-73-142-151-116.hsd1.ct.comcast.net [73.142.151.116]) (authenticated bits=0) by smtp01.srv.cs.cmu.edu (8.13.6/8.13.6) with ESMTP id u86Cu7Ju028624 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Tue, 6 Sep 2016 08:56:09 -0400 (EDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Subject: Re: [HoTT] A puzzle about "univalent equality" From: Dan Licata In-Reply-To: Date: Tue, 6 Sep 2016 08:56:07 -0400 Cc: Andrew Polonsky , Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> To: Michael Shulman X-Mailer: Apple Mail (2.3124) X-Scanned-By: mimedefang-cmuscs on 128.2.217.200 and the issue only comes up if you don=E2=80=99t have K, which would equate= (ap (=CE=BB u =E2=86=92 u True True) e) and Refl -Dan > On Sep 6, 2016, at 8:32 AM, Michael Shulman wrote: >=20 > Although, as Voevodsky showed, weak funext implies strong funext. >=20 > 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! >>=20 >>> I would be very surprised if there was something like this that was not= provable in "book HoTT=E2=80=9D. >>=20 >> 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. >>=20 >> 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 equivalenc= e, >> to make the transports compute. >>=20 >> Cheers, >> Andrew >>=20 >> -- >> 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. >=20 > --=20 > 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.