From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 22 Dec 2017 16:25:24 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: 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> <20171219153118.GA9218@mathematik.tu-darmstadt.de> <20171219163139.GB13875@mathematik.tu-darmstadt.de> <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_9469_1901569449.1513988724910" ------=_Part_9469_1901569449.1513988724910 Content-Type: multipart/alternative; boundary="----=_Part_9470_594670443.1513988724911" ------=_Part_9470_594670443.1513988724911 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Friday, December 22, 2017 at 4:20:21 PM UTC-5, Mart=C3=ADn H=C3=B6tzel E= scard=C3=B3=20 wrote: > > There may be some confusion about univalence and equality of subsets > of a type.=20 > > [...] > > Now, from a subset A : =E2=84=99 X, we get a type A' and an embedding A' = =E2=86=92 X. > (The construction works like this: we have A : X =E2=86=92 Prop, and a > projection Prop =E2=86=92 U. Then the type A' is the sum (=CE=A3) of comp= osite > function. The embedding is the first projection.) > > It is definitely not the case that if A'=3DB' for A,B : =E2=84=99 X then = A=3DB. > > [...] > > All the misunderstandings in the previous messages are caused by > looking at the particular type X=3D1 without enough care. > > And I think this is what Thomas is pointing out. > Huh? Your isEven/isOdd example is fine, but there, X =E2=89=A0 1. Is it not= the=20 case that if A'=3DB' for A,B : =E2=84=99 1 then A=3DB? (Note the specializa= tion to 1.) ------=_Part_9470_594670443.1513988724911 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Friday, December 22, 2017 at 4:20:21 PM UTC-5, Mart=C3= =ADn H=C3=B6tzel Escard=C3=B3 wrote:
There may be some confusion about univalence and equality of subset= s
of a type.=C2=A0

= [...]

Now, from a subset A : =E2=84=99 X, we get a type A' and an embedd= ing A' =E2=86=92 X.
(The construction works like this: we have A : X =E2= =86=92 Prop, and a
projection Prop =E2=86=92 U. Then the type A' is= the sum (=CE=A3) of composite
function. The embedding is the first pro= jection.)

It is definitely not the case that if A'=3DB'= ; for A,B : =E2=84=99 X then A=3DB.

[...]

All the misunderstandings in the previous messages are = caused by
looking at the particular type X=3D1 without enough care.

<= /span>
And I think this is what Thomas is pointing out.

Huh? Your isEven/isOdd example is= fine, but there, X =E2=89=A0 1. Is it not the case that if A'=3DB&= #39; for A,B : =E2=84=99 1 then A=3DB? (Note the specialization to 1.)
------=_Part_9470_594670443.1513988724911-- ------=_Part_9469_1901569449.1513988724910--