From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 24 Nov 2017 04:21:58 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] Yet another characterization of univalence MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_4495_1141354421.1511526118624" ------=_Part_4495_1141354421.1511526118624 Content-Type: multipart/alternative; boundary="----=_Part_4496_1748626521.1511526118624" ------=_Part_4496_1748626521.1511526118624 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit On 20/11/17 03:54, y wrote: > Can you elaborate on why it is true? 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 to > 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 = B. If (x:X, p : Id x = B) is in the fiber, then ap Sigma p : Sigma(Id x) = 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_4496_1748626521.1511526118624 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On 20/11/17 03:54, y wrote:
> Can you el= aborate on why it is true?=C2=A0

I am writing this= in Agda to be absolutely sure of all the
details. But this is go= ing slowly because lack of time. When It is
done I will give you = a link and also a proof in English prose.

> Als= o as this statement is similar
> to Yoneda's lemma, do we = have something like

> Also as this statement is= similar=C2=A0 to Yoneda's lemma, do we have
> something l= ike
> For a type X : U and B : X -> U, Id (X -> U) (Id X= x) B is equivalent to=C2=A0
> B x?

A= s 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

=C2=A0 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 f= iber, then

=C2=A0 =C2=A0ap Sigma p : Sigma(Id x) = =3D Sigma B,

and hence, being equal to a contracti= ble 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 (abo= ve
form of the) Yoneda Lemma and univalence, so show that this fi= ber is
equivalence to Sigma B (being a retract suffices, but we d= o in fact
get an equivalence automatically: it is laborious to ch= eck 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 a= ll types) you get univalence is subtler, and I
want to check ever= ything before I sketch an argument in public. But I
didn't wa= nt to do this if somebody told me, in response to the message
bel= ow, that this has been already done, but nobody did.

Martin

------=_Part_4496_1748626521.1511526118624-- ------=_Part_4495_1141354421.1511526118624--