From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 24 Nov 2017 11:11:37 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> In-Reply-To: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> References: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> Subject: Re: [HoTT] Yet another characterization of univalence MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_22700_243358649.1511550697283" ------=_Part_22700_243358649.1511550697283 Content-Type: multipart/alternative; boundary="----=_Part_22701_60025707.1511550697283" ------=_Part_22701_60025707.1511550697283 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Friday, 24 November 2017 12:21:58 UTC, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 wrote: > > On 20/11/17 03:54, y wrote: > > Can you elaborate on why it is true?=20 > Actually, my argument was fundamentally flawed, because this is not=20 provable. If univalence holds, then Id : X -> (X -> U) is an embedding. But If the K axiom holds, then again Id : X -> (X -> U) is an embedding. And hence there is no hope to deduce univalence from the fact that Id_X is= =20 an embedding for every X:U. (And, as a side remark, I can't see how to prove that Id_X is an embedding= =20 without using K or univalence.) Martin > I am writing this in Agda to be absolutely sure of all the > details. But this is going slowly because lack of time. When It is > done I will give you a link and also a proof in English prose. > > > Also as this statement is similar > > to Yoneda's lemma, do we have something like > > > Also as this statement is similar to Yoneda's lemma, do we have > > something like > > For a type X : U and B : X -> U, Id (X -> U) (Id X x) B is equivalent t= o=20 > > B x? > > As I said privately to you, yes. This follows from one of the Yoneda > Lemmas, namely that if Sigma B is contractible then the recursively > defined map > > Pi(y : Y), Id x y -> B y is an equivalence > > for every x : X and b : B x (and conversely). > > The Id-fiber of B is Sigma(x : X), Id x =3D B. > > If (x:X, p : Id x =3D B) is in the fiber, then > > ap Sigma p : Sigma(Id x) =3D Sigma B, > > and hence, being equal to a contractible type, Sigma B is > contractible. > > This doesn't use univalence or function extensionality. > > Next you have to use the contractibility of Sigma B to show that the > Id-fiber of B is contractible. It is this step which uses the (above > form of the) Yoneda Lemma and univalence, so show that this fiber is > equivalence to Sigma B (being a retract suffices, but we do in fact > get an equivalence automatically: it is laborious to check the > retraction condition; the section condition, which is not nedeed, is > much easier). > > With this you get that Id is an embedding. > > That from this (for all types) you get univalence is subtler, and I > want to check everything before I sketch an argument in public. But I > didn't want to do this if somebody told me, in response to the message > below, that this has been already done, but nobody did. > > Martin > > ------=_Part_22701_60025707.1511550697283 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable


On Friday, 24 November 2017 12:21:58 UTC, Mart=C3= =ADn H=C3=B6tzel Escard=C3=B3 wrote:
On 20/11/17 03:54, y wrote:
> Can= you elaborate on why it is true?=C2=A0

Actually, my argument was fundamentally flawed, because this is no= t provable.

If univalence holds, then Id : X ->= (X -> U) is an embedding.

But If the K axiom h= olds, then again Id : X -> (X -> U) is an embedding.

And hence there is no hope to deduce univalence from the fact that= Id_X is an embedding for every X:U.

(And, as a si= de remark, I can't see how to prove that Id_X is an embedding without u= sing K or univalence.)

Martin

=


=

I am writing this in Agda to be absolu= tely sure of all the
details. But this is going slowly because la= ck of time. When It is
done I will give you a link and also a pro= of in English prose.

> Also as this statement i= s similar
> to Yoneda's lemma, do we have something like

> Also as this statement is similar=C2=A0 to Yon= eda's lemma, do we have
> something like
> Fo= r a type X : U and B : X -> U, Id (X -> U) (Id X x) B is equivalent t= o=C2=A0
> B x?

As I said privately to= you, yes. This follows from one of the Yoneda
Lemmas, namely tha= t if Sigma B is contractible then the recursively
defined map

=C2=A0 Pi(y : Y), Id x y -> B y is an equivalence<= /div>

for every x : X and b : B x (and conversely).

The Id-fiber of B is Sigma(x : X), Id x =3D B.

If (x:X, p : Id x =3D B) is in the fiber, then
=
=C2=A0 =C2=A0ap Sigma p : Sigma(Id x) =3D Sigma B,

and hence, being equal to a contractible type, Sigma B is
contractible.

This doesn't use unival= ence or function extensionality.

Next you have to = use the contractibility of Sigma B to show that the
Id-fiber of B= is contractible. It is this step which uses the (above
form of t= he) Yoneda Lemma and univalence, so show that this fiber is
equiv= alence to Sigma B (being a retract suffices, but we do in fact
ge= t an equivalence automatically: it is laborious to check the
retr= action condition; the section condition, which is not nedeed, is
= much easier).

With this you get that Id is an embe= dding.

That from this (for all types) you get univ= alence is subtler, and I
want to check everything before I sketch= an argument in public. But I
didn't want to do this if someb= ody told me, in response to the message
below, that this has been= already done, but nobody did.

Martin
------=_Part_22701_60025707.1511550697283-- ------=_Part_22700_243358649.1511550697283--