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
--94eb2c122d0c220017053bd65661--