From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 24 Nov 2017 15:12:03 -0800 (PST)
From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?=
 <escardo...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <b8d32e71-d896-4962-a831-c1fd4a8280f7@googlegroups.com>
In-Reply-To: <CAHB0Dmn5=FxFNbA4nNXX5SJLaJdS8YGCtcvaheyPgCnBYVePyg@mail.gmail.com>
References: <e15c4ebe-12b3-4069-80d7-4de9ca6ccf80@googlegroups.com>
 <CAHB0Dmn5=FxFNbA4nNXX5SJLaJdS8YGCtcvaheyPgCnBYVePyg@mail.gmail.com>
Subject: Re: [HoTT] Yet another characterization of univalence
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_23641_1703845109.1511565123571"

------=_Part_23641_1703845109.1511565123571
Content-Type: multipart/alternative; 
	boundary="----=_Part_23642_550165889.1511565123571"

------=_Part_23642_550165889.1511565123571
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

You asked a question privately, but I choose to answer it here.

On Monday, 20 November 2017 03:54:55 UTC, Yuhao Huang wrote:
>
> Can you elaborate on why it is true? Also as this statement is similar to=
=20
> Yoneda's lemma, do we have something like=20
>
> For a type X : U and A : X -> U, Id (X -> U) (Id X x) A is equivalent to =
A=20
> x?
>
>
We have

 A x =E2=89=83 Nat (Id x) A           (yoneda)
     =3D =CE=A0(y:Y), Id x y =E2=86=92 A y  (definition)
     =E2=89=83 =CE=A0(y:Y), Id x y =E2=89=83 A y (because =CE=A3 A is contr=
actible (Yoneda corollary))
     =E2=89=83 =CE=A0(y:Y), Id x y =E2=89=A1 A y (by univalence)
     =E2=89=83 Id x =E2=89=A1 A y           (by extensionality)

Martin

=20

------=_Part_23642_550165889.1511565123571
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">You asked a question privately, but I choose to answer it =
here.<br><br>On Monday, 20 November 2017 03:54:55 UTC, Yuhao Huang  wrote:<=
blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-left: 0.8ex;bord=
er-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr">Can you elabor=
ate on why it is true? Also as this statement is similar to Yoneda&#39;s le=
mma, do we have something like=C2=A0<div><br></div><div>For a type X : U an=
d A : X -&gt; U, Id (X -&gt; U) (Id X x) A is equivalent to A x?</div></div=
><div><div class=3D"gmail_quote"><br></div></div></blockquote><div><br></di=
v><div>We have</div><div><br></div><div><div>=C2=A0A x =E2=89=83 Nat (Id x)=
 A=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(yoneda)</div><div>=C2=A0 =C2=A0=
 =C2=A0=3D =CE=A0(y:Y), Id x y =E2=86=92 A y=C2=A0 (definition)</div><div>=
=C2=A0 =C2=A0 =C2=A0=E2=89=83 =CE=A0(y:Y), Id x y =E2=89=83 A y (because =
=CE=A3 A is contractible (Yoneda corollary))</div><div>=C2=A0 =C2=A0 =C2=A0=
=E2=89=83 =CE=A0(y:Y), Id x y =E2=89=A1 A y (by univalence)</div><div>=C2=
=A0 =C2=A0 =C2=A0=E2=89=83 Id x =E2=89=A1 A y=C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0(by extensionality)</div></div><div><br></div><div>Martin</div=
><div><br></div><div>=C2=A0</div></div>
------=_Part_23642_550165889.1511565123571--

------=_Part_23641_1703845109.1511565123571--