From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 29 Nov 2017 14:16:22 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: 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_34257_955766197.1511993782738" ------=_Part_34257_955766197.1511993782738 Content-Type: multipart/alternative; boundary="----=_Part_34258_340566466.1511993782738" ------=_Part_34258_340566466.1511993782738 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. > > I like it. You say that (assuming funext) if idtoeq : (A B : U) -> A =3D B= =20 -> A =E2=89=83 B is a natural embedding (rather than a natural equivalence = as the=20 univalence axiom demands) then Id_X : X -> (X -> U) is an embedding for=20 all X:U. It is natural to ask whether the converse holds (particularly given my orig= inal wrong claim recorded in the subject of this thread). Do you think it d= oes? Martin =20 > Evan > > 2017-11-28 4:40 GMT-05:00 Andrej Bauer > >: > >> > If univalence holds, then Id : X -> (X -> U) is an embedding. >> > >> > But If the K axiom holds, then again Id : X -> (X -> U) is an embeddin= g. >> > >> > And hence there is no hope to deduce univalence from the fact that Id_= X=20 >> is >> > an embedding for every X:U. >> > >> > (And, as a side remark, I can't see how to prove that Id_X is an=20 >> embedding >> > without using K or univalence.) >> >> So you've invented a new axiom? >> >> Escardo's axiom: Id : X =E2=86=92 (X =E2=86=92 U) is an embedding. >> >> (We could call it Martin's axiom to create lots of confusion.) >> >> With kind regards, >> >> Andrej >> >> -- >> You received this message because you are subscribed to the Google Group= s=20 >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n=20 >> email to HomotopyTypeThe...@googlegroups.com . >> For more options, visit https://groups.google.com/d/optout. >> > > ------=_Part_34258_340566466.1511993782738 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.


I like it.=
 You say that (assuming funext) if idtoeq : (A B : U) -> A =3D B=20
-> A =E2=89=83 B is a natural embedding (rather than a natural equivalen=
ce as the=20
univalence axiom demands) then Id_X : X -> (X -> U) is an embedding f=
or=20
all X:U.

It is natural to ask whether the converse holds (particularly given my orig=
inal wrong claim recorded in the subject of this thread). Do you think it d=
oes?

Martin
=C2=A0
Evan

2017-11-28 4:40 GMT-05:00 Andrej Bauer <andr...@andrej.com>:
> If univalence holds, then Id : X -> (X -> U) is an embedding. >
> But If the K axiom holds, then again Id : X -> (X -> U) is an em= bedding.
>
> And hence there is no hope to deduce univalence from the fact that Id_= X is
> an embedding for every X:U.
>
> (And, as a side remark, I can't see how to prove that Id_X is an e= mbedding
> without using K or univalence.)

So you've invented a new axiom?

=C2=A0 Escardo's axiom: Id : X =E2=86=92 (X =E2=86=92 U) is an embeddin= g.

(We could call it Martin's axiom to create lots of confusion.)

With kind regards,

Andrej

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com= /d/optout.

------=_Part_34258_340566466.1511993782738-- ------=_Part_34257_955766197.1511993782738--