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-x23b.google.com (mail-oi1-x23b.google.com [IPv6:2607:f8b0:4864:20::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 276fbbc8 for ; Tue, 13 Nov 2018 20:36:35 +0000 (UTC) Received: by mail-oi1-x23b.google.com with SMTP id l204-v6sf7493047oia.17 for ; Tue, 13 Nov 2018 12:36:35 -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=geWagdVrxx/XPlkgJ1lm4GnfGX+/OyhaJauFcatDm8U=; b=eb+6+xNRPbIIFs3U/sfo72S7NcK11fyV3EXhSUy1oCC2QxKHpcsS5oOwU0uR9i+fx4 XHylvuZxeHl/MVW5TFdVhoO4F+Yf6yvmnzT/geKETyqig3/OdnelpC9DOliy7OTSfOMu 46BA3SE7r2QvBr4LnJijNLXGaevTWVRWv+21J27VXGoujVJuhlGXPU4zUqbFyWVcK178 QzpZuQcbq77wL3QNFTGNCMTrAmn0ZJikvNZUYodIaLGZabIUbtqqK+5dhtoYnAPUgF+D 760MKieKCTLQ260eHlGEJvSwptij1ot5tEjDZWZmrAW3rMcJ388nQkprAuFRqAF9BEw9 Rsaw== 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=geWagdVrxx/XPlkgJ1lm4GnfGX+/OyhaJauFcatDm8U=; b=JTVrNUxCG26j4IsFiqR0N2EaJWmyo9vWG5o2haT3BDkmEPP1dBtaqs6MJMJA75n4e0 4FymaybzEA+VLjrcJHJK3EEggvPDvrKmG8beVI9TZk69Q0bCCJXI3P4LVlB6gGdvUzHa 7/cEV/JPFvoXg+jtnjP8prKmrb56ClitwAajSpqJdIx/1afI3xvrQyLxKV3Og/2M+YwJ rJxWtJ+GqHanHCqEPxceGG8JTVQQUHFUvTqiu6lbjxiUYOhmsWKT5SoNYnbso/wL/nYP A8l3LLfWmxOGGXv6o1tiwaHtHYIJH7gopX/eUdmsXEqtj+GC5osj2QCsJX7CnPCWgLyA 4SCg== 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=geWagdVrxx/XPlkgJ1lm4GnfGX+/OyhaJauFcatDm8U=; b=mpbbw152oVxoCvr5sxWLc/DzuzKU/R3vtSuwnh3JoYPqyzH03sElZhXeEx47qdJNMd BwrjIVsovX+kE2nD59IEcwSfpWnHtyY/cXjaBVrCyrhvO7/gwDNxaifmtgC8VsWFv7D8 DoVn/nYM4sOcAr7r0BALy/KPe+eOgkbCDwt+/ZXz6rlKcMVxt4XJ98oIkn/mKvcb0av9 07i5e8pOjlrO0nPtXY2alNs3QX1ZnfvTM6lGRFRF43O1VBv/nTooqIcaethLyKwZPQLy FKF4d5TpkRE+J9V67szNVN3sIiU5l6fZa94d46EhPWcYBwYVv5N4w51wx0jAt4uzFmro SZyg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLt6AK48BQ3kTHuc3VMdgAUcHZ5eoLzlIA+bmx8eImLyfhcUru5 2rRyrTYTn1Lk/WedtbF+/BI= X-Google-Smtp-Source: AJdET5f/f7k020kZrHVW8aeI0axUDxqddhbdlwwrb4u+BMhi1PKvbyMz7RUK00gyAhAo5D1cGeYMZA== X-Received: by 2002:a9d:da3:: with SMTP id 32mr128242ots.3.1542141394143; Tue, 13 Nov 2018 12:36:34 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:ecc:: with SMTP id 70ls6185407otj.1.gmail; Tue, 13 Nov 2018 12:36:33 -0800 (PST) X-Received: by 2002:a9d:da3:: with SMTP id 32mr128241ots.3.1542141393594; Tue, 13 Nov 2018 12:36:33 -0800 (PST) Date: Tue, 13 Nov 2018 12:36:32 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <9e20f45d-49ab-4e4e-a488-91cf24a115fb@googlegroups.com> In-Reply-To: <0090c5e9-8e11-484c-953c-bf2958d03b72@googlegroups.com> References: <0090c5e9-8e11-484c-953c-bf2958d03b72@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_1152_308247815.1542141393087" 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_1152_308247815.1542141393087 Content-Type: multipart/alternative; boundary="----=_Part_1153_1617354402.1542141393087" ------=_Part_1153_1617354402.1542141393087 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable NB. Of course this map is left-cancellable. But this is weaker than being= =20 an embedding. M. On Tuesday, 13 November 2018 20:32:22 UTC, 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)? > > Martin > > --=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_1153_1617354402.1542141393087 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
NB. Of course this map is left-cancellable. But this is we= aker than being an embedding. M.

On Tuesday, 13 November 2018 20:32:= 22 UTC, 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
<= br>
=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=A0A=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
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 the map =F0=9D=9F=99 =E2=86=92 = =F0=9D=93=A4 with constant value =F0=9D=9F=99.

=C2= =A0 =C2=A0 In general, a function =F0=9D=9F=99 =E2=86=92 X into a type X is= *not* an
=C2=A0 =C2=A0 embedding. Such a function is an embeddin= g iff it maps the
=C2=A0 =C2=A0 point of =F0=9D=9F=99 to a point = x:X such that the type x=3Dx is a
=C2=A0 =C2=A0 singleton.
<= div>
=C2=A0 =C2=A0 And indeed for X:=3D=F0=9D=93=A4 we have t= hat 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 the identity map = =F0=9D=93=A4 =E2=86=92 =F0=9D=93=A4, which, being an equivalence, is an
=C2=A0 =C2=A0 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)?

Martin

<= /div>

--
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_1153_1617354402.1542141393087-- ------=_Part_1152_308247815.1542141393087--