From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.25.17.156 with SMTP id 28mr3236655lfr.2.1473147035367;
        Tue, 06 Sep 2016 00:30:35 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.153.76 with SMTP id b73ls1651975wme.18.gmail; Tue, 06 Sep
 2016 00:30:34 -0700 (PDT)
X-Received: by 10.28.209.3 with SMTP id i3mr2915099wmg.7.1473147034662;
        Tue, 06 Sep 2016 00:30:34 -0700 (PDT)
Return-Path: <andrew....@gmail.com>
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 p199si650949wmd.1.2016.09.06.00.30.34
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Tue, 06 Sep 2016 00:30:34 -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 u14so17019139lfd.1
        for <HomotopyT...@googlegroups.com>; Tue, 06 Sep 2016 00:30:34 -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=xchwQPckyTitML5U3hHqyoxE0aJRR7KK/hxkSMDYfHY=;
        b=AZNDKCmCIduDp1iJUUGG3FLfIhSVyWc1lEv7AE86jk9rdNT8B6AaXdlOYUACJ+hph2
         rIpgTxR7YN9ziEk0k4ivU1qrFBnstotjHZwq9GgdUhTYaUvTlr5Jz1ukKM1PicrghQ74
         +B+D3yVsGVBFcRHB2uM4S4+V0k6o1ik7VW0lzYbAt3mpmKtczONFE/VJvIzPpvqgVu51
         /nwj04KG/QEWDRQLHje8TnhYKxFasXyo24AHR9x9LZhoOLTHlcj5S2NrS/mC+U2FAFsl
         ZTSXR5lA5W4bEkqWJ4DLv7mJCabyl8P1Df+hORxh4qWZr07LaZgZ5hyk9ao0JUN8RkbE
         teYw==
X-Gm-Message-State: AE9vXwM2Ysu8kZIAYP/1U9lkvvRvKbZOLA9WZGDsOrsnQUBukVzOHcx0ahsJcxC2XBdlOK3LcywNH7ciTKvPcQ==
X-Received: by 10.25.234.1 with SMTP id i1mr2943520lfh.84.1473147034334; Tue,
 06 Sep 2016 00:30:34 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.25.83.143 with HTTP; Tue, 6 Sep 2016 00:30:33 -0700 (PDT)
In-Reply-To: <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu>
References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu>
From: Andrew Polonsky <andrew....@gmail.com>
Date: Tue, 6 Sep 2016 09:30:33 +0200
Message-ID: <CABcT7WBZo8bt6dtfDowd2nOYrtLPwsCC4Yxara1sZ5_oHeUQFw@mail.gmail.com>
Subject: Re: [HoTT] A puzzle about "univalent equality"
To: Dan Licata <d...@cs.cmu.edu>
Cc: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

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 p=
rovable 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