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-x33d.google.com (mail-ot1-x33d.google.com [IPv6:2607:f8b0:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 23da158a for ; Tue, 13 Nov 2018 23:47:42 +0000 (UTC) Received: by mail-ot1-x33d.google.com with SMTP id j15sf9750110ota.17 for ; Tue, 13 Nov 2018 15:47:42 -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=GSQHZew6yt/KM9Jo2rIgU+LLFCSDk6fQK37ny/Rp+D0=; b=dF2Ymy9QgNx5rIhZPiJ5NDGRVNDJDQerjS2Es8d53q9E2lhbCh+zl6t2wLMwLT4q6L wiuApSlxk8V7n3MwYEu81+6ejbPLCFqxy71CZmxbDMpLAPmvN13GDQSIQ7CP1nKBEt8N zb3HI84zVUM26UEiEmzDT1jVms0foKVNlSRQWn179jst5cauJ5/bn6XD5DJ5jT7cuOBH JzEetrABR/c79p+QueLbUeM6Hz0dtkEc1n6Rrz5L+u232ytgxTEDCRPzxfgLp/YHpivL 6ORYbChLe5KoSsxNuM1ymRdqCdRxCmcAqgo+R4l4TY/SP9wRsb8mksffy0ZaAW+/fQN5 raHw== 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=GSQHZew6yt/KM9Jo2rIgU+LLFCSDk6fQK37ny/Rp+D0=; b=Swe973UsrQ1aul0GlW3mq9RdYTH6WsiuBnqYrOqLeWo2mgLxItYOyikMAU4CpNgp3O 0WrHvyVd+zFsPLgELpTELDno4B5Lbs4IaM0VZ5YoO2tWkbkCcLQ0ZisP/z71R+KsPsLJ iYlxVsg2MhoxdEQxG5DYUXefr/fZDJpryo0M8IjZiCKpIP04E6ltL1ytb4e4MkCuzW2m XkMkh4a5Zh5/WG3NaSWgshbFt1hkTRMINxTHKPOQXFh9QWdDnpUqOfLgGlymxoOZrAPi xnTNiYrS9pW7Hti8v9F+SOD65XNokT/Q4SlaOcCSviJqweLmeidmK9VwME4eZG/QhIBM NPBA== 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=GSQHZew6yt/KM9Jo2rIgU+LLFCSDk6fQK37ny/Rp+D0=; b=CV9mSG39hRv6AGfpeAoWhcbjm1XZF2lpbXRMCS/1y0kA5xKW9MIFEvvfo3eBXVXCTJ OSMjvPjURm29jDa4Yrt3ejEapP1LgvrdVJ+F3coTmpFHLepOVQAxhWDD8vlyYZO2CvIj AQa8fX9AkvP8SlWs3b+bqDBXJoZewS1ysTEaY+HsWVTIuiJT5AH66O8Jolp5ngobW00G QI6Dl7AofroT+WSZpTA7gP4S8hhkq1itzcJDMx+BiUUkxJ+verZzTEQDa9KT19pNsm8Q 69bG1jbwkA8+3BjxJHStPseno6U/GA7Tb7pcdNFeDC7E2s3yuifgBJDyQlL/Yz2OpHCc cuUg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKP34RJeY+8LCSozbrTEtwtxUvOlpF+P6Ijl5G8wIT/VljvQwqY cxh3ZcRSssqK0M49caWKcu4= X-Google-Smtp-Source: AJdET5cPQG0WmhF3t4hwqiBD57rfBu7mbnvjCTrQxQCz+vA28eidyh2romPo9+Px4lCHopQyx+QoOA== X-Received: by 2002:aca:c703:: with SMTP id x3mr1990oif.5.1542152861144; Tue, 13 Nov 2018 15:47:41 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:d40f:: with SMTP id l15ls1441393oig.6.gmail; Tue, 13 Nov 2018 15:47:40 -0800 (PST) X-Received: by 2002:aca:4892:: with SMTP id v140-v6mr12764oia.1.1542152860802; Tue, 13 Nov 2018 15:47:40 -0800 (PST) Date: Tue, 13 Nov 2018 15:47:40 -0800 (PST) From: Jean Joseph To: Homotopy Type Theory Message-Id: <0472bc2b-0212-48b9-bfe7-fb98c7916763@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_2858_1881547490.1542152860277" X-Original-Sender: jsjean00@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_2858_1881547490.1542152860277 Content-Type: multipart/alternative; boundary="----=_Part_2859_522283227.1542152860277" ------=_Part_2859_522283227.1542152860277 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I think to show this is an embedding may imply the law of double negation.= =20 For any proposition Q, let P =3D {0 : Z | Q}. Let A be defined as for all p= :=20 P, A(p) =3D 0 : P, and let B be defined as for all p : P, B(p) =3D not not = (0 :=20 P). To show that Pi (p : P), A(p) =3D Pi (p : P), B(p), you can define the= =20 following isomorphism (?): for any f : Pi (p : P), A(p), define g : Pi (p := =20 P), B(p) by picking p : P, then f(p) : A(p), so Q is true. Hence, not not Q= =20 is true, meaning it has an element, so g(p) is that element. We then can=20 conclude A =3D B. By function extensionality, that's equivalent to for all = p=20 : P, A (p) =3D B (p), which gives Q =3D not not Q.=20 Jean On Tuesday, November 13, 2018 at 3:32:22 PM UTC-5, Mart=C3=ADn H=C3=B6tzel = Escard=C3=B3=20 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_2859_522283227.1542152860277 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I think to show this is an embedding may imply the la= w of double negation. For any proposition Q, let P =3D {0 : Z | Q}. Let A b= e defined as for all p : P, A(p) =3D 0 : P, and let B be defined as for all= p : P, B(p) =3D not not (0 : P). To show that Pi (p : P), A(p) =3D Pi (p := P), B(p), you can define the following isomorphism (?): for any f : Pi (p = : P), A(p), define g : Pi (p : P), B(p) by picking p : P, then f(p) : A(p),= so Q is true. Hence, not not Q is true, meaning it has an element, so g(p)= is that element. We then can conclude A =3D B. By function extensionality,= that's equivalent to for all p : P, A (p) =3D B (p), which gives Q =3D= not not Q.=C2=A0

Jean

On Tuesday, Novemb= er 13, 2018 at 3:32:22 PM UTC-5, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote= :
Let P b= e a subsingleton and =F0=9D=93=A4 be a universe, 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=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
fiber= s.)

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 equivale= nt 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 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=3Dx 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 sing= leton.

(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 a= n 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
d= istinction (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_2859_522283227.1542152860277-- ------=_Part_2858_1881547490.1542152860277--