From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.159.245.134 with SMTP id a6mr200446pls.44.1511993734518; Wed, 29 Nov 2017 14:15:34 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.98.150.22 with SMTP id c22ls6744694pfe.1.gmail; Wed, 29 Nov 2017 14:15:33 -0800 (PST) X-Received: by 10.101.97.166 with SMTP id i6mr205992pgv.170.1511993733493; Wed, 29 Nov 2017 14:15:33 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1511993733; cv=none; d=google.com; s=arc-20160816; b=I2xXVK8UPr3hjaHRrUwo+3ex4SFRG8FJueT41dwKmavcbJAoR+ikdddx+Y2k3/innD 2900HAJNelMhpQ5nHERyJgJENL2O1HMi7o5aKXRtYfmlcY3hie5zY0DliEi9VMC8TyNR EAr1EATR1FT+jHu2lAz5kYHzfHPSSuIcxGcEP86e4kA24rvVh0J4rlEWdL8tJ5x3wQ9P 5ZkP6XV99UMG0vCbj2xF+ONXk2UZ3Su2A6oSIZbM42AZzvdrCT+wJNWwy6npmWzmc/1k xkkfS9OFWW4XiqUv4oldMJ+gEo9GqbRMNTSyun79nN6wy0aAbX3kR3XPJ/TpM+dUxlIV VBxg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=UrGDkaFdS4VOWn8x1UHPW96tnDAs+zPPKxXsNx1DYzs=; b=BbWHJTMHinetFzXdzBHPivy3Q/+gRW7eTEQ7Ul3DOZ5dGHGYw2Y0ARpC+8AjbHF4k7 8HVxEDUwlJvYOiY2cVFRdT6Gb0DApzC8UXKkvMy5VKAjLnHX1WIoX+ub6kGODp+tynqK nWoOkz5+SsAVN1sWb9Xgxcb5UCJ3hLSe4rq9rsp3b5/xt7G1nLAQLBEc0izhYLc+vJxh j6GzNwrWS8yxh3jkXMseufo5e01nlxjjATkOxUQC0nTZPGGkt+zqNRd/gmrZQDi8/l1F n4K/ZIbwpymDLuAJcx5D+RHCyOzh/umnwL4KbM/inx9WUYVWPGZM+7jNtvItaPAhQhm1 JnjQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=mQNUsVUA; spf=pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c05::231 as permitted sender) smtp.mailfrom=evanc...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yw0-x231.google.com (mail-yw0-x231.google.com. [2607:f8b0:4002:c05::231]) by gmr-mx.google.com with ESMTPS id b6si161758plm.3.2017.11.29.14.15.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 29 Nov 2017 14:15:33 -0800 (PST) Received-SPF: pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c05::231 as permitted sender) client-ip=2607:f8b0:4002:c05::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=mQNUsVUA; spf=pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c05::231 as permitted sender) smtp.mailfrom=evanc...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-yw0-x231.google.com with SMTP id g191so1971454ywe.7 for ; Wed, 29 Nov 2017 14:15:33 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=UrGDkaFdS4VOWn8x1UHPW96tnDAs+zPPKxXsNx1DYzs=; b=mQNUsVUAsAZCdGOJaT+O55rc2Ht+us8wDYWkB37ajtvVVh0fTlc7GL6ErNV0mrbKlX icf0L3t7MfxioVgie3PqD+Ve+taCZu+olSvrOUmJKXZXzGkkmuOGjcNJlDgEajxeVzZ/ 6ahLUYRABQPCQMcadyf86QQtY7PsQTvGAcblK4L0JIijF7tEit2cbMHp0sont8FQX161 o3eCUhuPVvYnvxuGdXIpavQm+L5LPwD5iJmwkxCLhdbx9NGfRGM4xMmTBkQKg2JZFxeS dZy/8LNnfGOy8TF/+/JMkX6us4aP8Fj/+lBPTfnlQajjlxQiOLpIkg75slIKaFMhEbQ4 QUew== X-Gm-Message-State: AJaThX4+en25GqUDjDHJ8Sz9Blu+rusVyM7F+H5pDiIiTmMH6cadkX11 k1EjYsPNRzJeOLYShkekd9iP8RK7yo+fGNsvnL0jpQ== X-Received: by 10.129.124.135 with SMTP id x129mr249662ywc.509.1511993732535; Wed, 29 Nov 2017 14:15:32 -0800 (PST) MIME-Version: 1.0 Received: by 10.37.139.140 with HTTP; Wed, 29 Nov 2017 14:15:32 -0800 (PST) In-Reply-To: <204e382a-efcf-cb13-006f-47fdbadd99a5@cs.bham.ac.uk> References: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> <204e382a-efcf-cb13-006f-47fdbadd99a5@cs.bham.ac.uk> From: Evan Cavallo Date: Wed, 29 Nov 2017 17:15:32 -0500 Message-ID: Subject: Re: [HoTT] Yet another characterization of univalence To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="001a11493512549a23055f267920" --001a11493512549a23055f267920 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > > Can you show the converse? > I don't think so (or at least, I don't see how it could be done). Evan 2017-11-29 17:12 GMT-05:00 Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 : > > > On 29/11/17 21:12, Evan Cavallo wrote: > >> 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 holds.= Since Id x >> y is always equivalent to (=CE=A0(z:X), Id x z =E2=89=83 Id y z), showin= g 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 > -> A =E2=89=83 B is a natural embedding (rather than an equivalence as th= e > univalence axiom demands) then Id_X : X -> (X -> U) is an embedding for a= ll > X:U. > > Can you show the converse? > > Martin > > > >> Evan >> >> 2017-11-28 4:40 GMT-05:00 Andrej Bauer > andrej...@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 >> embedding. >> > >> > 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 >> 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 >> Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, >> send an email to HomotopyTypeThe...@googlegroups.com >> . >> For more options, visit https://groups.google.com/d/optout >> . >> >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com > HomotopyTypeThe...@googlegroups.com>. >> For more options, visit https://groups.google.com/d/optout. >> > > -- > http://www.cs.bham.ac.uk/~mhe > --001a11493512549a23055f267920 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Can= you show the converse?

I don't t= hink so (or at least, I don't see how it could be done).

E= van

2017-11-29= 17:12 GMT-05:00 Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 <= ;m.es...@cs.bham= .ac.uk>:


On 29/11/17 21:12, Evan Cavallo wrote:
Maybe this is interesting: assuming funext, if the canonical map Id A B -&g= t; A =E2=89=83 B is an embedding for all A,B, then Martin's axiom holds= . Since Id x y is always equivalent to (=CE=A0(z:X), Id x z =E2=89=83 Id y = z), showing that it is equivalent to Id (Id x) (Id y) can be reduced to sho= wing 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 -> A =E2=89=83 B is a natural embedding (rather than an equivalence a= s the univalence axiom demands) then Id_X : X -> (X -> U) is an embed= ding for all X:U.

Can you show the converse?

Martin



Evan

2017-11-28 4:40 GMT-05:00 Andrej Bauer <andrej...@andrej.com <mailto:andrej...@andrej.com&= gt;>:

=C2=A0 =C2=A0 > If univalence holds, then Id : X -> (X -> U) is an= embedding.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > But If the K axiom holds, then again Id : X -> (X -&g= t; U) is an embedding.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > And hence there is no hope to deduce univalence from the= fact that Id_X is
=C2=A0 =C2=A0 > an embedding for every X:U.
=C2=A0 =C2=A0 >
=C2=A0 =C2=A0 > (And, as a side remark, I can't see how to prove tha= t Id_X is an embedding
=C2=A0 =C2=A0 > without using K or univalence.)

=C2=A0 =C2=A0 So you've invented a new axiom?

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

=C2=A0 =C2=A0 (We could call it Martin's axiom to create lots of confus= ion.)

=C2=A0 =C2=A0 With kind regards,

=C2=A0 =C2=A0 Andrej

=C2=A0 =C2=A0 --
=C2=A0 =C2=A0 You received this message because you are subscribed to the G= oogle
=C2=A0 =C2=A0 Groups "Homotopy Type Theory" group.
=C2=A0 =C2=A0 To unsubscribe from this group and stop receiving emails from= it,
=C2=A0 =C2=A0 send an email to HomotopyTypeTheory+unsubscribe@googlegro= ups.com
 =C2=A0 =C2=A0 <mailto:HomotopyTypeTheory%2Bunsubs...@googlegroups.c= om>.
=C2=A0 =C2=A0 For more options, visit https://groups.google.com/d/= optout
 =C2=A0 =C2=A0 <https://groups.google.com/d/optout>.=


--
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+unsubscribe@googlegroups.com <mailto:= H= omotopyTypeTheory+unsubsc...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.

--
http://www.cs.bham.ac.uk/~mhe

--001a11493512549a23055f267920--