From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 24 Nov 2017 15:28:18 -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: <4cc1b669-72f1-4dae-9ea6-5190f9b4c261@googlegroups.com>
In-Reply-To: <b8d32e71-d896-4962-a831-c1fd4a8280f7@googlegroups.com>
References: <e15c4ebe-12b3-4069-80d7-4de9ca6ccf80@googlegroups.com>
 <CAHB0Dmn5=FxFNbA4nNXX5SJLaJdS8YGCtcvaheyPgCnBYVePyg@mail.gmail.com>
 <b8d32e71-d896-4962-a831-c1fd4a8280f7@googlegroups.com>
Subject: Re: [HoTT] Yet another characterization of univalence
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_23939_678172532.1511566098987"

------=_Part_23939_678172532.1511566098987
Content-Type: multipart/alternative; 
	boundary="----=_Part_23940_2034741824.1511566098987"

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

Of course the last line is Id x =E2=89=A1 A (without the y).=20
Copy-and-paste-and-don't-modify properly phenomenon.=20

On Friday, 24 November 2017 23:12:03 UTC, Mart=C3=ADn H=C3=B6tzel Escard=C3=
=B3 wrote:
>
>
>  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 con=
tractible (Yoneda=20
> 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)
>
>
Lat line should have been=20

         =E2=89=83 Id x =E2=89=A1 A
=20

> Martin
>
> =20
>

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

<div dir=3D"ltr">Of course the last line is Id=C2=A0x =E2=89=A1 A (without =
the y). Copy-and-paste-and-don&#39;t-modify properly phenomenon.=C2=A0<br><=
br>On Friday, 24 November 2017 23:12:03 UTC, Mart=C3=ADn H=C3=B6tzel Escard=
=C3=B3  wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-l=
eft: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr"=
><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 contractib=
le (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 extensio=
nality)</div></div><div><br></div></div></blockquote><div><br></div><div>La=
t line should have been=C2=A0</div><div><br></div><div>=C2=A0 =C2=A0 =C2=A0=
 =C2=A0 =C2=A0=E2=89=83 Id x =E2=89=A1 A</div><div>=C2=A0</div><blockquote =
class=3D"gmail_quote" style=3D"margin: 0;margin-left: 0.8ex;border-left: 1p=
x #ccc solid;padding-left: 1ex;"><div dir=3D"ltr"><div></div><div>Martin</d=
iv><div><br></div><div>=C2=A0</div></div></blockquote></div>
------=_Part_23940_2034741824.1511566098987--

------=_Part_23939_678172532.1511566098987--