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-x238.google.com (mail-oi1-x238.google.com [IPv6:2607:f8b0:4864:20::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5cbd8210 for ; Tue, 13 Nov 2018 20:32:26 +0000 (UTC) Received: by mail-oi1-x238.google.com with SMTP id n3-v6sf3625855oia.3 for ; Tue, 13 Nov 2018 12:32:26 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=kmHKJu+oGOAGb5Q6Gj2wGn3UtjNE6WvL+24T6lKa+04=; b=nR7JhmUIgDqGnbd8fxdZyH/WCa/sRxzdm+682FkM46I4KLvDwm1k7RwH4tRjBHiIa+ awEGLZBmCeRlLQYBMqVQTzL3n+ilSnkuQKIauSfx9lG2uzV/vSvza/QzbSSk0Uc/Pnx6 eloT3LFPq9qWobtfVwx+wj19Juu+HuvHmFburmuKP52aXe3hJq8CV3gdaXOuYSWDz/O/ o/+uCPCNXf4Ffr5IMYN6aeznsqWin+LAx4cDq1vMMTdkerl4rAUa+X9xXJMNXkwIF6kC ipkWxNJabxp26Z4OnzJ9jbnuPndaIkNqKGYsFIEM0dHeomcpopTbQ13KSWJxZOMsiHV4 EKVQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kmHKJu+oGOAGb5Q6Gj2wGn3UtjNE6WvL+24T6lKa+04=; b=amy4vZAFqQaU080KAUI+GObRN4ygHrlWc2Vr5vU94ljQ58ObyNN7rp58tq2myAE+Pm YmSPsUaSfr9yCabRgEA6ghMbg3PSDRY+1M1jYoVwtg1EaPxNO+KN1zl/F+/W3HgQyUTu XSnfAqOnjbHfsm5I8nfWjGwJl60UQNlQBABVn12/akR+RAY0Grz92bEEYLurf0ItJgD7 ln3ouzp+aP395XrraL0rX1o19ABudDzptM73tVufe1yKr1YjqihdCcHzY+IdTCZIBADI 1ejeo4wDCV0B59MhQG1AqKMo9PKSh9uWdNIdU5JbGkxa1d/8vwUwFXNmgZbo+EcA49Oq T1CQ== 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: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=kmHKJu+oGOAGb5Q6Gj2wGn3UtjNE6WvL+24T6lKa+04=; b=gRk6pMDdY/MJCbpKp4RXKG5mOd27AyZPqvDBLud0OxHrdwy6y55O49Q2fQN6X/g/Nx WpLm8zsjPJ7CFEh3nC4C/ktOTs17NFbLybC0nQ1TB0hvI7C+Ln/1kxtP7UWeo2b35pAe V4WZMqyaR0xo28oe+02BAGpBFlfYXxsjegvM3NnARwB926Q+axERfeo3Um09GAMb62QW pOkNLwo7Fn1PHU21CjHvOdKNO0gmn1MrLhr50lUyK2+FoN9ZETEMpN8vzlPt0wZwwfXx gZsqR6sQG1NTVMovFUt8dK/MJTM/bS47HRTa/cb2itWztbZJbWU4RFKY7piaHtfDrIni wA3g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLgpN6MJvR/RGbJb+2X+8HdlVSSsZ7qQD7VohdWWWZ+8EO7U2jW 3mQUhwK3VG1ZfngxPrVW2fY= X-Google-Smtp-Source: AJdET5fO6SglJzunBUPlOanVa3VygQI40u6hgtcT9yNfnPB0XBkldIDUbkMTE4AV/ak8Sy3FahZNaA== X-Received: by 2002:aca:5803:: with SMTP id m3-v6mr7361oib.4.1542141145347; Tue, 13 Nov 2018 12:32:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:3c11:: with SMTP id q17ls2480209otc.12.gmail; Tue, 13 Nov 2018 12:32:25 -0800 (PST) X-Received: by 2002:a9d:5403:: with SMTP id j3mr126591oth.2.1542141144506; Tue, 13 Nov 2018 12:32:24 -0800 (PST) Date: Tue, 13 Nov 2018 12:32:22 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <0090c5e9-8e11-484c-953c-bf2958d03b72@googlegroups.com> Subject: [HoTT] Proof that something is an embedding without assuming excluded middle? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2644_4698659.1542141142494" 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_2644_4698659.1542141142494 Content-Type: multipart/alternative; boundary="----=_Part_2645_1393437603.1542141142494" ------=_Part_2645_1393437603.1542141142494 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 e= quivalence, 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_2645_1393437603.1542141142494 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Let P be a subsingleton and =F0=9D=93=A4 be a univers= e, and consider the
product map

=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 fundam= entally different:

(0) If P=3D=F0=9D=9F=98, the do= main 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 fu= nction =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 embedding iff it maps the
=C2=A0 =C2=A0 point of =F0=9D=9F=99 to a point x:X such that the type x=3D= x is a
=C2=A0 =C2=A0 singleton.

=C2=A0 = =C2=A0 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 amou= nts 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 embed= ding.

Question. Is there a uniform proof that =CE= =A0 as above for P a
subsingleton is an embedding, without consid= ering the case
distinction (P=3D=F0=9D=9F=98)+(P=3D=F0=9D=9F=99)?=

Martin

--
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_2645_1393437603.1542141142494-- ------=_Part_2644_4698659.1542141142494--