From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 18d24476 for ; Wed, 14 Nov 2018 19:00:34 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id 32sf5988556ots.15 for ; Wed, 14 Nov 2018 11:00:34 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=llWxse8AMY6it8JuzLe+Y3LPhD16d9qOyDWPmlApYw0=; b=kgoAEOFx++YxybsJgyOeID3zbJGNWg1tMm3QkVAy5SWG2uCmAUrBrwqdLUDsh8VWRX dTszLtwLZTOYxM5/8p3a8dRKLRwTxQDChqINDWdofSP9TjLD4pcTOsgJisARardhxQw+ U34PDKO/1gz2aCXqL0xNESkX7tt7Ad0/zYjPaV5xftP8ASW0UaHSiur0l97zkEdHgb+M Kb59Twk+RYU/cXOv6rv/oIRnMhAv7u8N5V8atOe/cLhEE+R5IcO9AVdIqpANp/ztw5k9 2W5BXnZwbaS9zqadCDGiD/5HOFlvPyo0jgszKSjWP8RlNmp0qPBj2BvgbeFcwT27thRk o+5w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=llWxse8AMY6it8JuzLe+Y3LPhD16d9qOyDWPmlApYw0=; b=iEPhaeOr1UHJxkFnf1u1X1EXS6ca2OxXkKFAKF+EF43m5Gk5D1gJQuOjEosu+tdixX Q5x4plyyHu1e0VCwtm86cNa1S2X9ih/iMz3YFdccyFKT2y9jM2OTRPqXa4q4cmVHWAwL yZjI9f7pWDq0Ajegu1ePkLy9X4Ofom6/LqQFlFTfNpBjqsuSs/525J4fu/0ecet+JXEK UpEOGVzPcdW7oNUSHvfZANktJtOXN7H+D7utHtohuhbaU+2OaDjHlUPIHHkv1Nbr/0Sd UVQelvfHwunptC9CV11EPCAHo+tlIS088WyH2kRJFGIZUeHxWh5buK8w+u3fYmonQBo2 rY0g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=llWxse8AMY6it8JuzLe+Y3LPhD16d9qOyDWPmlApYw0=; b=hLofjdDeWKt+dc43MHMw3wwVM0ef++5IL6y+W6gmmpYZz6/OM2tJBcunA3ZOluv9jz RxEXm7m7dOMlmq09hwbjLFXkzrMQGtkYx0kOyq4Y9ciNTLmK0upfawGqRfNjO9/6L3Gg GrrmMilWkZjUrBizDWRR///prEEU5/oUGQU+Xmgm9GAUnjZ68rjHx2Ftvm/TjQJLCU6h BJgjFwOO4MJrvGHON9icBqbBFUr+wbafj+LsJHQ3CWSYoUBs/MeAoe+MmV2+0WMePChs j3u5edk+YJz1p6zDy1/q1YBYrmeeQWHgt+75OFlk0YMnPrSZxgU7ZSwS5siUkj2iDpqy +LKw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKwMkEUz769LqghlqxUE38ZQEM+hzQQgZtfr1i8F5U047WnWJ/1 lTVbAbl0tUpD434IvZ+EarM= X-Google-Smtp-Source: AJdET5dE3f3PP1DsKqSyXXphbFTP3dNL9SVUMHguS4XrGfoXUpSUn5N5dCws1q/X4xZVaNEeCJShYg== X-Received: by 2002:a9d:2c22:: with SMTP id f31mr79406otb.4.1542222033489; Wed, 14 Nov 2018 11:00:33 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:20e6:: with SMTP id x93ls7367716ota.15.gmail; Wed, 14 Nov 2018 11:00:33 -0800 (PST) X-Received: by 2002:a9d:da3:: with SMTP id 32mr81248ots.3.1542222032817; Wed, 14 Nov 2018 11:00:32 -0800 (PST) Date: Wed, 14 Nov 2018 11:00:32 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <54115bb8-270b-4e04-a1a4-016d01e1c1f9@googlegroups.com> In-Reply-To: <5b276491-e7b8-442a-b76a-d395f8e916a6@googlegroups.com> References: <0090c5e9-8e11-484c-953c-bf2958d03b72@googlegroups.com> <0472bc2b-0212-48b9-bfe7-fb98c7916763@googlegroups.com> <5b276491-e7b8-442a-b76a-d395f8e916a6@googlegroups.com> Subject: [HoTT] Re: Proof that something is an embedding without assuming excluded middle? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_72_1160439144.1542222032161" X-Original-Sender: escardo.martin@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_72_1160439144.1542222032161 Content-Type: multipart/alternative; boundary="----=_Part_73_540124067.1542222032161" ------=_Part_73_540124067.1542222032161 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks, Paolo.=20 Independently, Mike Shulman had sent me another solution based on modal=20 operators off-list. But these two solutions are essentially the same.=20 I am glad the answer to the question is positive.=20 Maybe I'll explain later why I am interested in this question.=20 Best,=20 Martin=20 On Wednesday, 14 November 2018 11:07:50 UTC, Paolo Capriotti wrote: > > On Tue, 13 Nov 2018, at 8:32 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wro= te: > > Let P be a subsingleton and =F0=9D=93=A4 be a universe, and consider th= e > > product map > > > > =CE=A0 : (P =E2=86=92 =F0=9D=93=A4) =E2=86=92 =F0=9D=93=A4 > > A =E2=86=A6 =CE=A0 (p:P), A(p). > > > > Is this an embedding? (In the sense of having subsingleton > > fibers.) > > > > It is easy to see that this is the case if P=3D=F0=9D=9F=98 or P=3D=F0= =9D=9F=99 (empty or > > singleton type). > > > > But the reasons are fundamentally different: > > > > (0) If P=3D=F0=9D=9F=98, the domain of =CE=A0 is equivalent to =F0=9D= =9F=99, and =CE=A0 amounts to > > the map =F0=9D=9F=99 =E2=86=92 =F0=9D=93=A4 with constant value =F0= =9D=9F=99. > > > > In general, a function =F0=9D=9F=99 =E2=86=92 X into a type X is *n= ot* an > > embedding. Such a function is an embedding iff it maps the > > point of =F0=9D=9F=99 to a point x:X such that the type x=3Dx is a > > singleton. > > > > And indeed for X:=3D=F0=9D=93=A4 we have that the type =F0=9D=9F=99= =3D=F0=9D=9F=99 is a singleton. > > > > (1) If P=3D=F0=9D=9F=99, the domain of =CE=A0 is equivalent to =F0=9D= =93=A4, and =CE=A0 amounts to > > the identity map =F0=9D=93=A4 =E2=86=92 =F0=9D=93=A4, which, being = an equivalence, is an > > embedding. > > > > Question. Is there a uniform proof that =CE=A0 as above for P a > > subsingleton is an embedding, without considering the case > > distinction (P=3D=F0=9D=9F=98)+(P=3D=F0=9D=9F=99)? > > I think one can show that ap =CE=A0 is an equivalence by giving an invers= e.=20 > Given X, Y : P =E2=86=92 =F0=9D=93=A4, first note that the equality type = X =3D Y is equivalent=20 > by function extensionality to (u : P) =E2=86=92 X u =3D Y u. Since one ca= n prove=20 > easily that (u : P) =E2=86=92 X u =3D =CE=A0 X, it follows that X =3D Y i= s equivalent to P =E2=86=92=20 > =CE=A0 X =3D =CE=A0 Y. Hence we get a map =CF=89 : =CE=A0 X =3D =CE=A0 Y = =E2=86=92 X =3D Y. To show that it is=20 > indeed an inverse of ap =CE=A0, start with some =CE=B1 : =CE=A0 X =3D =CE= =A0 Y. By following the=20 > construction above, we get that ap =CE=A0 (=CF=89 =CE=B1) maps a function= h : =CE=A0 X to =CE=BB u .=20 > =CE=B1 (=CE=BB v . tr^X [u,v] (h u)) u, where [u,v] : u =3D v is given by= the fact that=20 > P is a proposition. Now, within the assumption u : P, the =CE=BB expressi= on in=20 > brackets is equal to h itself, hence ap =CE=A0 (=CF=89 =CE=B1) =3D =CE=B1= . The other composition=20 > is easier, since it can just be checked on reflexivity. > > Best, > Paolo > > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_73_540124067.1542222032161 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks, Paolo.=C2=A0

Independently, Mik= e Shulman had sent me another solution=20 based on modal operators off-list. But these two solutions are=20 essentially the same.

I am glad the answer to the question is positive.

Maybe I'll explain later why I am interested in this question.

Best,
Martin=C2=A0

On Wednesday, 14 November 2018 11:07:50 UTC, Paolo = Capriotti wrote:
On Tue, 13 Nov 2018, at 8:32 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 wrote:
> Let P be a subsingleton and =F0=9D=93=A4 be a uni= verse, and consider the
> product map
>
>=C2=A0 =C2=A0=CE=A0 : (P =E2=86=92 =F0=9D=93=A4) =E2=86=92 =F0=9D=93= =A4
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 A=C2=A0 =C2=A0 =C2=A0= =E2=86=A6 =CE=A0 (p:P), A(p).
>
> Is this an embe= dding? (In the sense of having subsingleton
> fibers.)
>
> It is easy to see that this is the case if P=3D=F0= =9D=9F=98 or P=3D=F0=9D=9F=99 (empty or
> singleton type).
>
> But the reasons are fundamentally different:
>
> (0) If P=3D=F0=9D=9F=98, the domain of =CE=A0 is= equivalent to =F0=9D=9F=99, and =CE=A0 amounts to
>=C2=A0 =C2= =A0 =C2=A0the map =F0=9D=9F=99 =E2=86=92 =F0=9D=93=A4 with constant value = =F0=9D=9F=99.
>
>=C2=A0 =C2=A0 =C2=A0In general, = a function =F0=9D=9F=99 =E2=86=92 X into a type X is *not* an
>= ;=C2=A0 =C2=A0 =C2=A0embedding. Such a function is an embedding iff it maps= the
>=C2=A0 =C2=A0 =C2=A0point of =F0=9D=9F=99 to a point x:X= such that the type x=3Dx is a
>=C2=A0 =C2=A0 =C2=A0singleton.=
>
>=C2=A0 =C2=A0 =C2=A0And indeed for X:=3D=F0= =9D=93=A4 we have that the type =F0=9D=9F=99=3D=F0=9D=9F=99 is a singleton.=
>
> (1) If P=3D=F0=9D=9F=99, the domain of =CE= =A0 is equivalent to =F0=9D=93=A4, and =CE=A0 amounts to
>=C2= =A0 =C2=A0 =C2=A0the identity map =F0=9D=93=A4 =E2=86=92 =F0=9D=93=A4, whic= h, being an equivalence, is an
>=C2=A0 =C2=A0 =C2=A0embedding.=
>
> Question. Is there a uniform proof that =CE= =A0 as above for P a
> subsingleton is an embedding, without c= onsidering the case
> distinction (P=3D=F0=9D=9F=98)+(P=3D=F0= =9D=9F=99)?

I think one can show that ap =CE=A0 is= an equivalence by giving an inverse. Given X, Y : P =E2=86=92 =F0=9D=93=A4= , first note that the equality type X =3D Y is equivalent by function exten= sionality to (u : P) =E2=86=92 X u =3D Y u. Since one can prove easily that= (u : P) =E2=86=92 X u =3D =CE=A0 X, it follows that X =3D Y is equivalent = to P =E2=86=92 =CE=A0 X =3D =CE=A0 Y. Hence we get a map =CF=89 : =CE=A0 X = =3D =CE=A0 Y =E2=86=92 X =3D Y. To show that it is indeed an inverse of ap = =CE=A0, start with some =CE=B1 : =CE=A0 X =3D =CE=A0 Y. By following the co= nstruction above, we get that ap =CE=A0 (=CF=89 =CE=B1) maps a function h := =CE=A0 X to =CE=BB u . =CE=B1 (=CE=BB v . tr^X [u,v] (h u)) u, where [u,v]= : u =3D v is given by the fact that P is a proposition. Now, within the as= sumption u : P, the =CE=BB expression in brackets is equal to h itself, hen= ce ap =CE=A0 (=CF=89 =CE=B1) =3D =CE=B1. The other composition is easier, s= ince it can just be checked on reflexivity.

Best,<= /div>
Paolo

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_73_540124067.1542222032161-- ------=_Part_72_1160439144.1542222032161--