From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.69.10 with SMTP id s10mr5958868lja.1.1473165163326; Tue, 06 Sep 2016 05:32:43 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.215.39 with SMTP id o39ls721737lfg.25.gmail; Tue, 06 Sep 2016 05:32:42 -0700 (PDT) X-Received: by 10.25.141.85 with SMTP id p82mr5939911lfd.10.1473165162614; Tue, 06 Sep 2016 05:32:42 -0700 (PDT) Return-Path: Received: from mail-lf0-x234.google.com (mail-lf0-x234.google.com. [2a00:1450:4010:c07::234]) by gmr-mx.google.com with ESMTPS id b189si614873wmg.0.2016.09.06.05.32.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 06 Sep 2016 05:32:42 -0700 (PDT) Received-SPF: neutral (google.com: 2a00:1450:4010:c07::234 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2a00:1450:4010:c07::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2a00:1450:4010:c07::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-lf0-x234.google.com with SMTP id g62so144907477lfe.3 for ; Tue, 06 Sep 2016 05:32:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=ot/aKJxW+Rce9jYy4FnFegLEVR5PiVtwlar4BarG07w=; b=S0MYFJNdQNfjG5qWuNtmRSXZiVht0JdSNK8RQQl9AIEULTGlBBNAPfQQ1q9YVyLiIU Bz43Kyo0x2BXR2Ozj4MinGh2hrOAUdLhjD0Hbx2iO3+vM37SjYQxux/41PJ8fmJjfOuw uQLiq7TI+hir2aO+xQSSPWbewfNWv4c+6iscid9vsdQURNRgRAh4hzQA7zMc4JyDDrCQ 4k0W2H2w/FGWXucU4tcEUxLPpthEeY3ifoIIBf6osxU4D4+HmFIrgtDIy7Xhd40yDa86 TA75cVFjdwjSgN+lgh8nTLeRN9XMSiCenTBQI9rMLvE0bbgW7vZJUhz7gwc4KJQ3cbWt Kn3w== X-Gm-Message-State: AE9vXwMG70teyxBm1ezEAxhjECpnCukczGpEaAkiAvVnS/MxA12PvpSysgFPagLcWa+Cnmww X-Received: by 10.46.69.9 with SMTP id s9mr7946821lja.7.1473165161922; Tue, 06 Sep 2016 05:32:41 -0700 (PDT) Return-Path: Received: from mail-lf0-f50.google.com (mail-lf0-f50.google.com. [209.85.215.50]) by smtp.gmail.com with ESMTPSA id r190sm5624348lfg.49.2016.09.06.05.32.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 06 Sep 2016 05:32:41 -0700 (PDT) Received: by mail-lf0-f50.google.com with SMTP id l131so51380038lfl.2 for ; Tue, 06 Sep 2016 05:32:41 -0700 (PDT) X-Received: by 10.25.215.35 with SMTP id o35mr12461053lfg.40.1473165160424; Tue, 06 Sep 2016 05:32:40 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Tue, 6 Sep 2016 05:32:19 -0700 (PDT) In-Reply-To: References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> From: Michael Shulman Date: Tue, 6 Sep 2016 05:32:19 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A puzzle about "univalent equality" To: Andrew Polonsky Cc: Dan Licata , Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Although, as Voevodsky showed, weak funext implies strong funext. 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=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 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.