From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 1 Dec 2017 06:53:25 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <86619505-c082-4c11-8d5d-9159e1b351ec@googlegroups.com> In-Reply-To: References: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> Subject: Re: [HoTT] Yet another characterization of univalence MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_948_1567041298.1512140005652" ------=_Part_948_1567041298.1512140005652 Content-Type: multipart/alternative; boundary="----=_Part_949_870406635.1512140005652" ------=_Part_949_870406635.1512140005652 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Wednesday, 29 November 2017 21:13:27 UTC, E Cavallo wrote: > > Maybe this is interesting: assuming funext, if the canonical map Id A B -= >=20 > A =E2=89=83 B is an embedding for all A,B, then Martin's axiom holds. Sin= ce Id x y=20 > is always equivalent to (=CE=A0(z:X), Id x z =E2=89=83 Id y z), showing t= hat it is=20 > equivalent to Id (Id x) (Id y) can be reduced to showing that the map Id= =20 > (Id x) (Id y) -> (=CE=A0(z:X), Id x z =E2=89=83 Id y z) is an embedding. > > Id A B -> A =E2=89=83 B is an embedding both if univalence holds and if a= xiom K=20 > holds. > OK. Here is a further weakening of the hypotheses. It suffices to have funext (again) and that the map idtofun{B}{C} : A=3DB =E2=86=92 (A=E2=86=92B) is left-cancellable (that is, idtofun p =3D idtofun q =E2=86=92 p=3Dq). Univalence gives that this is an embedding, which is stronger than saying that it is left-cancellable. And also K gives that this is an embedding. Here is the proof that these assumptions suffice. To show that Id : X=E2=86=92(X=E2=86=92U) is an embedding, let A : X=E2=86= =92U. It suffices to show that the type T :=3D =CE=A3(x:X), Id x =3D A is a proposition. To this end, it is in turn enough to show that T =E2=86=92 isProp T. So let (x=E2=82=80:X, p=E2=82=80: Id x =3D A) : T. Then ap =CE=A3 p=E2=82=80 : =CE=A3(Id x=E2=82=80) =3D =CE=A3 A, where =CE= =A3{X} : (X=E2=86=92U)=E2=86=92U. Because the type =CE=A3(Id x=E2=82=80) of paths from x=E2=82=80 is contract= ible, so is the type =CE=A3 A by transport. For x:X arbitrary, we have maps Id x =3D A (1) =E2=86=92 (happly) =CE=A0(y:X), Id x y =3D A x (2) =E2=86=92 (induced by idtofun) =CE=A0(y:X), Id x y =E2=86=92 A x (3) =E2=86=92 (evaluate at x and idpath x)=20 A x If funext holds, then the map (1) is left-cancellable because it is an equivalence. The map idtofun : Id x y =3D A x =E2=86=92 (A x y =E2=86=92 A x) is left-ca= ncellable by assumption. The induced map (2) is then also left-cancellable assuming funext. The map (3) is an equivalence assuming funext, and hence left-cancellable. Left-cancellable maps are closed under composition, and hence we get a left-cancellable map f x : Id x =3D A =E2=86=92 A x But then also the map g : (=CE=A3(x:X), Id x A) =E2=86=92 =CE=A3 A defined by g(x,p) =3D (x, f x p) is left-cancellable (easy to check, in the general form that if f i : B i =E2=86=92 C i is a family of left cancellable maps then the map (i,b) =E2=86=A6 (i,f i b) : =CE=A3 B =E2=86= =92 =CE=A3 C is left-cancellable). But for any left-cancellable map into a proposition, its domain is a proposition. Hence (=CE=A3(x:X), Id x A) is a proposition because =CE=A3 A, being contractible, is a proposition. This concludes the proof that T =E2=86=92 isProp T and hence that Id is an embedding. Martin ------=_Part_949_870406635.1512140005652 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable


On Wednesday, 29 November 2017 21:13:27 UTC, E Cav= allo wrote:
<= div>Maybe this is interesting: assuming funext, if the canonical map Id A B= -> A =E2=89=83 B is an embedding for all A,B, then Martin's axiom h= olds. Since Id x y is always equivalent to (=CE=A0(z:X), Id x z =E2=89=83 I= d y z), showing that it is equivalent to Id (Id x) (Id y) can be reduced to= showing that the map Id (Id x) (Id y) -> (=CE=A0(z:X), Id x z =E2=89=83= Id y z) is an embedding.

Id A B -> A =E2=89=83= B is an embedding both if univalence holds and if axiom K holds.


=C2=A0OK. Here is a furth= er weakening of the hypotheses. It suffices to have
funext (again= ) and that the map

=C2=A0 =C2=A0 idtofun{B}{C} : A= =3DB =E2=86=92 (A=E2=86=92B)

is left-cancellable (= that is, idtofun p =3D idtofun q =E2=86=92 p=3Dq).

Univalence gives that this is an embedding, which is stronger than
saying that it is left-cancellable. And also K gives that this is an
embedding.


Here is the proof= that these assumptions suffice.

To show that Id := X=E2=86=92(X=E2=86=92U) is an embedding, let A : X=E2=86=92U.
It suffices to show that the type T :=3D =CE=A3(x:X), Id x =3D= A is a
proposition.

To this end, it is = in turn enough to show that T =E2=86=92 isProp T.

= So let (x=E2=82=80:X, p=E2=82=80: Id x =3D A) : T.

Then ap =CE=A3 p=E2=82=80 : =CE=A3(Id x=E2=82=80) =3D =CE=A3 A, where =CE= =A3{X} : (X=E2=86=92U)=E2=86=92U.

Because the type= =CE=A3(Id x=E2=82=80) of paths from x=E2=82=80 is contractible, so is the<= /div>
type =CE=A3 A by transport.

For x:X arbi= trary, we have maps

=C2=A0 =C2=A0 =C2=A0 Id x =3D = A
(1) =E2=86=92=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 (happly)
=C2=A0 =C2=A0 =C2=A0 =CE=A0(= y:X), Id x y =3D A x
(2) =E2=86=92=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 (induced by idtofun)
=C2=A0 =C2=A0 =C2=A0 =CE=A0(y:X), Id x y =E2=86=92 A x
(3) =E2= =86=92=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 (evaluate at x and idpath x)=C2=A0
=C2=A0 =C2=A0 =C2=A0 A= x

If funext holds, then the map (1) is left-cance= llable because it is an
equivalence.

The= map idtofun : Id x y =3D A x =E2=86=92 (A x y =E2=86=92 A x) is left-cance= llable by
assumption. The induced map (2) is then also left-cance= llable assuming
funext.

The map (3) is a= n equivalence assuming funext, and hence
left-cancellable.
<= div>
Left-cancellable maps are closed under composition, and = hence we get
a left-cancellable map

=C2= =A0 =C2=A0 =C2=A0f x : Id x =3D A=C2=A0 =C2=A0=E2=86=92=C2=A0 =C2=A0A x

But then also the map

=C2=A0= =C2=A0 =C2=A0g : (=CE=A3(x:X), Id x A) =E2=86=92 =CE=A3 A

defined by g(x,p) =3D (x, f x p) is left-cancellable (easy to chec= k, in
the general form that if f i : B i =E2=86=92 C i is a famil= y of left
cancellable maps then the map (i,b) =E2=86=A6 (i,f i b)= : =CE=A3 B =E2=86=92 =CE=A3 C is
left-cancellable).
But for any left-cancellable map into a proposition, its domai= n is a
proposition. Hence (=CE=A3(x:X), Id x A) is a proposition = because =CE=A3 A,
being contractible, is a proposition.

This concludes the proof that T =E2=86=92 isProp T and henc= e that Id is an
embedding.

Martin
<= div>
------=_Part_949_870406635.1512140005652-- ------=_Part_948_1567041298.1512140005652--