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-oi1-x240.google.com (mail-oi1-x240.google.com [IPv6:2607:f8b0:4864:20::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 21aebc5d for ; Wed, 14 Nov 2018 11:07:52 +0000 (UTC) Received: by mail-oi1-x240.google.com with SMTP id w80sf555028oiw.19 for ; Wed, 14 Nov 2018 03:07:52 -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=zkDe/18IkICkNd9NGqX7bTNLxAwoFn0if1C0N7HeiFE=; b=nA1rrtN/5zUzmW5XnWLxSYy94yIlyII7l4Cm/CX+vKlp5EWTG1LSgmxC5Uh2n07U6y zRtWC0jUMMHhv/4GwMGEDqtpwSSvE/2drxRZkNYZy5zy0w3nCrHpBG7zbaHmecBRgZdQ hhl/qA15LqfFu5/zDFxR8dw5VKHHi/CY+Rn9GnDq7mmWkxBjRktTarfLH/sekmB1Jxl9 fz1tzvwu4o2ml4qnOEZTzKBUtxdMAglxjHCm8I/tSPqiJ0d22qFODjzTq4RZyW5iecKK h00NsEtJOlniQWjy9D+7y2G4QRX9W9n9xlFsJE2TzyWEfVBO28lfY976mJrqSSaQo4fI UlnA== 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=zkDe/18IkICkNd9NGqX7bTNLxAwoFn0if1C0N7HeiFE=; b=SnqBEiQU9EHQDSjm2cDIXdltUrP1iNik4sg0PQDBT7T083xDKJSeXQwaS7rsZuULtF 9m2sEYWMavra/i/JCLPu12xusn3Ap7dowcYOxomXqFGfZQSsp2sKIaU9+MChEogwyLwY 0xLTyD5Y/3zaB85sqGZTjQF9QvdmH5L7PsoevnWmtmjYyU75oy/KE3aFDHfYTPMUpDRH bgk5VmFX5mcwNu7L/LJUAB6qcI8RaPu2nmnmDmjTu4tpI5F/FDvGYCvI/kIH1v4ybqGT W98Zdn94h3Eb9AqRDSNKxOiJc29RAuxARqAj600SUTuhudrmdjldN7F6ZM7tLZnJrmZl KY9Q== 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=zkDe/18IkICkNd9NGqX7bTNLxAwoFn0if1C0N7HeiFE=; b=b3krvlYhpG33OVWYdOJdNrMieBmgqPLVl2Bh9s9jn6qN/wJR8f8qo+KghJEVE5ZLh1 w9+iAT4ze0kXAL3LsmrP1rgsMuJw7VSH0DhmXL5Fcbhhf+EawT1RBuJhd2CWGQ35oq8m YTRH1SDBcOhex8BkLT4BkEoIyI6qJQaPbEmtBV/2PQf9WEF4JN9K7uO6TjcJt0bvEAkV p0NJ/eQCjZBCtt3xJDcuSgSHT0F0dwqqUtEOh5ySTeUG6Ty19u+l4XMUVJH3lYqq5dm8 JZjUv6pCkh0xHXRtqY+rYwHLxjlQjVp0eqNB+NMpZDpRfWTM0bS5ZTh71ltb4BJyNQMa jr+w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIE45putpq3XVkkGDaUkReeqUY5FOGi11cxoAEWOHl+NJKDnj+E paW9H4a7ZQhahbuP8obKjXs= X-Google-Smtp-Source: AJdET5dFbB0FuvZOfsx9k0ubRxoVq7NVJq3dAHb2tDkchham91QoU+YXRj+nT5eTD3eqDx7HXsp7VQ== X-Received: by 2002:aca:4892:: with SMTP id v140-v6mr54332oia.1.1542193671646; Wed, 14 Nov 2018 03:07:51 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:5f46:: with SMTP id t67-v6ls6706796oib.5.gmail; Wed, 14 Nov 2018 03:07:51 -0800 (PST) X-Received: by 2002:aca:308d:: with SMTP id w135mr31425oiw.0.1542193671224; Wed, 14 Nov 2018 03:07:51 -0800 (PST) Date: Wed, 14 Nov 2018 03:07:50 -0800 (PST) From: Paolo Capriotti To: Homotopy Type Theory Message-Id: <5b276491-e7b8-442a-b76a-d395f8e916a6@googlegroups.com> In-Reply-To: References: <0090c5e9-8e11-484c-953c-bf2958d03b72@googlegroups.com> <0472bc2b-0212-48b9-bfe7-fb98c7916763@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_1402_964059727.1542193670486" X-Original-Sender: p.capriotti@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_1402_964059727.1542193670486 Content-Type: multipart/alternative; boundary="----=_Part_1403_1797084469.1542193670486" ------=_Part_1403_1797084469.1542193670486 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 universe, and consider the > 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 *not= * 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 inverse.= =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 can = prove=20 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=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 t= he fact that=20 P is a proposition. Now, within the assumption u : P, the =CE=BB expression= 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_1403_1797084469.1542193670486 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Tue, 13 Nov 2018, at 8:32 PM, Mart=C3=ADn H=C3=B6t= zel Escard=C3=B3 wrote:
> Let P be a subsingleton and =F0=9D= =93=A4 be a universe, 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 embedding? (In the sense of having subsingleton
> fib= ers.)
>
> 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 dif= ferent:
>
> (0) If P=3D=F0=9D=9F=98, the domain o= f =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 const= ant 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 i= ff 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=A0= singleton.
>
>=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 si= ngleton.
>
> (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
&g= t;=C2=A0 =C2=A0 =C2=A0the identity map =F0=9D=93=A4 =E2=86=92 =F0=9D=93=A4,= which, being an equivalence, is an
>=C2=A0 =C2=A0 =C2=A0embed= ding.
>
> Question. Is there a uniform proof that= =CE=A0 as above for P a
> subsingleton is an embedding, witho= ut 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 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 ex= tensionality to (u : P) =E2=86=92 X u =3D Y u. Since one can prove easily t= hat (u : P) =E2=86=92 X u =3D =CE=A0 X, it follows that X =3D Y is equivale= nt 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= construction 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= assumption u : P, the =CE=BB expression in brackets is equal to h itself, = hence ap =CE=A0 (=CF=89 =CE=B1) =3D =CE=B1. The other composition is easier= , since it can just be checked on reflexivity.

Bes= t,
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_1403_1797084469.1542193670486-- ------=_Part_1402_964059727.1542193670486--