From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 22 Dec 2017 13:20:21 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <84edd3f3-4d2b-4864-a7bd-808cebcef72f@googlegroups.com> In-Reply-To: <700E969A-9BB6-496E-8CB1-0230E099F085@exmail.nottingham.ac.uk> 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> Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_9515_699349864.1513977621248" ------=_Part_9515_699349864.1513977621248 Content-Type: multipart/alternative; boundary="----=_Part_9516_327162795.1513977621249" ------=_Part_9516_327162795.1513977621249 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable There may be some confusion about univalence and equality of subsets of a type.=20 Univalence is compatible with the fact that two subsets A,B of a type X are equal iff they have the same elements. In fact, univalence implies that. Define Prop=3D=CE=A3(P : U),isProp P where isProp(P:U) =3D =CE=A0(x,y:P),x= =3Dy. This is a large type (it lives in the same universe as U, rather than in U). You may wish to make this small (like in UniMath), or not, but this is orthogonal to this discussion. Then define the powerset of a type X by =E2=84=99 X =3D X =E2=86=92 Prop. (As in topos theory.) Then for A : =E2=84=99 X and x : X we write x =E2=88=88 A to mean A x. (As in the internal language of a topos.) 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.) Without assuming univalence, we can't prove (or disprove) this equality. Not in intensional MLTT, or even in so-called extensional MLTT (=3D intensional MLTT + equality reflection). This is because in order to prove this equality, we need both functional and propositional extensionality. Extensional MLTT has the former but not the latter. Univalent MLTT has both. Here, the quantifier =E2=88=80 is a function of type (X =E2=86=92 Prop) =E2= =86=92 Prop and the logical connective _=E2=87=94_ is a function Prop =E2=86=92 Prop =E2=86=92 = Prop (or Prop =C3=97 Prop =E2=86=92 Prop, it doesn't matter). 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 compos= ite 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. Example: X=3D=E2=84=95, A=3DisEven and B=3DisOdd. Then A =E2=89=A0 B but A'= =3DB' (because A' and B' are isomorphic sets). However, we do have that =E2=84=99 X =E2=89=83 =CE=A3 (A' : U), =CE=A3 (e : A' =E2=86=92 X), isEmb= edding e, where (isEmbedding e) means that the fibers of e are propositions. Then the elements (=CE=A3 isEven, (_ , _)) and (=CE=A3 isOdd, (_ , _)) of t= he rhs type, for uniquely determined "_", are different, even though the types =CE=A3 isEven and =CE=A3 isOdd are equal. 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. Best, Martin ------=_Part_9516_327162795.1513977621249 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
There may be some confusion about univalence and equality of subsets
of a type.=C2=A0

Univalence is compatible with the fac= t that two subsets A,B of a type
X are equal iff they have the same e= lements.

In fact, univalence implies that.

is a large type (it lives in the same universe as U, rath= er than in
U). You may wish to make this small (like in UniMath), or = not, but
this is orthogonal to this discussion.

Then= define the powerset of a type X by =E2=84=99 X =3D X =E2=86=92 Prop.
(As in topos theory.)

Then for A : =E2=84=99 X and x : X = we write x =E2=88=88 A to mean A x.
(As in the internal language of a= topos.)

Then, assuming univalence, we have (theorem of in= tensional MLTT+UA):

=C2=A0 (A=3DB) =3D =E2=88=80(x:X), x = =E2=88=88 A =E2=87=94 x =E2=88=88 B.

(Because the middle e= quality is that of two sets, we don't need to
<= font color=3D"#000000">worry about which s= pecific equality we pick - there is at most
one. This again relies on= univalence.)

= Without assuming univalence, we can't = prove (or disprove) this
equality. Not in intensional MLTT, or even i= n so-called extensional
MLTT (=3D intensional MLTT + equality reflect= ion). This is because in
order to prove this equality, we need both f= unctional and
propositional extensionality. Extensional MLTT has th= e former but not
the latter. Univalent MLTT has both.

logical connective _=E2=87=94_ is a function P= rop =E2=86=92 Prop =E2=86=92 Prop (or Prop =C3=97
<= font color=3D"#000000">Prop =E2=86=92 Prop= , it doesn't matter).
<= span style=3D"font-size: 14px;">
Now, from a subset A : =E2=84=99= X, we get a type A' and an embedding A' =E2=86=92 X.=
(The co= nstruction works like this: we have A : X =E2=86=92 Prop, and a
proje= ction Prop =E2=86=92 U. Then the type A' is the sum (=CE=A3) of composi= te
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.

= Example: X=3D=E2=84=95, A=3DisEven and B= =3DisOdd. Then A =E2=89=A0 B but A'=3DB' (because A'
and = B' are isomorphic sets).

However, we do have that
=C2=A0 =E2=84=99 X =E2=89=83 =CE=A3 (A' : U), =CE=A3 (e : = A' =E2=86=92 X), isEmbedding e,

where (isEmbedding e) = means that the fibers of e are propositions.

=
Then the elem= ents (=CE=A3 isEven, (_ , _)) and (=CE=A3 isOdd, (_ , _)) of the
rhs = type, for uniquely determined "_", are different, even though the=
types =CE=A3 isEven and =CE=A3 isOdd are equal.
<= div>
All= the misunderstandings in the previous messages are caused by=
looking= at the particular type X=3D1 without enough care.
=
=
And I t= hink this is what Thomas is pointing out.

Best,
Mart= in


------=_Part_9516_327162795.1513977621249-- ------=_Part_9515_699349864.1513977621248--