From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 22 Dec 2017 13:36:48 -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: <1784992e-f8cd-4e49-9231-1f3a470854ea@googlegroups.com>
In-Reply-To: <84edd3f3-4d2b-4864-a7bd-808cebcef72f@googlegroups.com>
References: <20171218115228.GB29410@mathematik.tu-darmstadt.de>
 <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk>
 <CAB0nkh1s1Z_Fdn8_btnb+0auM+OfiYTuAmqaGdmAkEKfkhnOuQ@mail.gmail.com>
 <A336FB3E-8247-4240-A034-3119B1C516FB@exmail.nottingham.ac.uk>
 <20171219153118.GA9218@mathematik.tu-darmstadt.de>
 <D55DEF85-61F6-480E-B627-B59CE5DBD481@exmail.nottingham.ac.uk>
 <20171219163139.GB13875@mathematik.tu-darmstadt.de>
 <A4B921E2-1AC8-474B-BE7E-6FEC68ADBB68@exmail.nottingham.ac.uk>
 <20171220110052.GC8054@mathematik.tu-darmstadt.de>
 <5B8F4A6C-DD7C-4A14-812C-4AEA35C41BEA@exmail.nottingham.ac.uk>
 <20171220114104.GG8054@mathematik.tu-darmstadt.de>
 <318cbeff-e7f2-4c45-b3c4-f392a94dd09d@googlegroups.com>
 <700E969A-9BB6-496E-8CB1-0230E099F085@exmail.nottingham.ac.uk>
 <84edd3f3-4d2b-4864-a7bd-808cebcef72f@googlegroups.com>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof
 irrelevance consistent?
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_9273_1289824429.1513978608350"

------=_Part_9273_1289824429.1513978608350
Content-Type: multipart/alternative; 
	boundary="----=_Part_9274_900178160.1513978608350"

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

Correction (that you already spotted, of course):

On Friday, 22 December 2017 21:20:21 UTC, Mart=C3=ADn H=C3=B6tzel Escard=C3=
=B3 wrote:
>
>
> Then, assuming univalence, we have (theorem of intensional MLTT+UA):
>
>   (A=3DB) =3D =E2=88=80(x:X), x =E2=88=88 A =E2=87=94 x =E2=88=88 B.
>
> (Because the middle equality is that of two sets, we don't need to
> worry about which specific equality we pick - there is at most
> one. This again relies on univalence.)
>

It is an equality of two *propositions*, of course, which is what I meant=
=20
to say.

M.
=20

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

<div dir=3D"ltr">Correction (that you already spotted, of course):<br><br>O=
n Friday, 22 December 2017 21:20:21 UTC, Mart=C3=ADn H=C3=B6tzel Escard=C3=
=B3  wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-left=
: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr"><d=
iv><br></div><div><font color=3D"#000000"><span style=3D"font-size:14px">Th=
en, assuming univalence, we have (theorem of intensional MLTT+UA):</span></=
font></div><div><font color=3D"#000000"><span style=3D"font-size:14px"><br>=
</span></font></div><div><font color=3D"#000000"><span style=3D"font-size:1=
4px">=C2=A0 (A=3DB) =3D =E2=88=80(x:X), x =E2=88=88 A =E2=87=94 x =E2=88=88=
 B.</span></font></div><div><font color=3D"#000000"><span style=3D"font-siz=
e:14px"><br></span></font></div><div><font color=3D"#000000"><span style=3D=
"font-size:14px">(Because the middle equality is that of two sets, we don&#=
39;t need to</span></font></div><div><font color=3D"#000000"><span style=3D=
"font-size:14px">worry about which specific equality we pick - there is at =
most</span></font></div><div><font color=3D"#000000"><span style=3D"font-si=
ze:14px">one. This again relies on univalence.)</span></font></div></div></=
blockquote><div><br></div><div>It is an equality of two *propositions*, of =
course, which is what I meant to say.</div><div><br></div><div>M.</div><div=
>=C2=A0<br></div></div>
------=_Part_9274_900178160.1513978608350--

------=_Part_9273_1289824429.1513978608350--