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 19713e80 for ; Thu, 15 Nov 2018 22:26:45 +0000 (UTC) Received: by mail-oi1-x240.google.com with SMTP id s140sf8442146oih.4 for ; Thu, 15 Nov 2018 14:26:44 -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=6gtCYWBFemmFBA2DAW0fyC7VuRp1lLbwRp+76uLX67U=; b=sqO7luWsc+5i11wj770UnPuoUrR8R5lj4Z+oVQKyaIqwK4/zWj2Oaft52WhoNp6JKG 7At3WEc2Q4IIBDY+L2rz/FwIMsnyzogFIFDoA4UEhxiJPQTui1wucdQhQU2Cb6jXCyvz bdibAnpp5POlSC5rSmWXa1iHurdVyOUJan8NEQLTfdfBmoV+UxUxAaQLCPkpoxa/ZDxx AcPRMAcw6W0+A3jgEcy0Nww02F4OzHrbpnzoRkINWi4powubsHRYOE3jzVouhFRfCE4t 3ISN5DXTYzzxMf/S9CoWSVBxXRtH9NMrDlh93tjnsJTXOQ3xHo7E1iwIp5YymS9hz7pP CyNw== 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=6gtCYWBFemmFBA2DAW0fyC7VuRp1lLbwRp+76uLX67U=; b=lmvZO8Lrk8xEe3V84TXzyTEUQ5wolUDzAE5gQMnPCVaWMx+ybFW5mXrXkgaWRIuyQS Wor7vYhTUkHHqnSuel2aPUHHBn2HO6tzN4Pl1qlztxLM6L5AAH9ZGGcIHoq0I2elP6T6 uWV8vU17v5MmwMGx3fYn6Idc+J7rcVqJoCqKExUWMX9fNAcPVCSan/b8F9+FxSbfYcob 7bDo12YQDlxPtIWSyFclsyO6WYQ3PVSU6tHE5cqaqwatEb1eKOpqlW7oxdI5cJqVRkKa X6rTYdJW1BzzLWM+D6Xp29SuVMrB4ir73hZ2H/TK55o4pENzNBhEQS4a6ATBiRvN7Bs7 2Eug== 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=6gtCYWBFemmFBA2DAW0fyC7VuRp1lLbwRp+76uLX67U=; b=blXiMcoDo4Gi4QyhBlSJQRRHt5Ii63SSDvfB5BS/HNdbJlebLoJJivDbhjDvos1DuI sQXg37tZxuaQqfKpLQp5BkakZh63mCUIJUFlx31CnpTEdBWhQgyO5cqQgc4VSJilrEKu J9wSsD2/6d5BUOD6MBWByRysuL3smkaJcyHGjWATtnHtP/3PihCW/bNxutol+sN8aXnE 2A0xlNWxXZSEuw66PXF+eItN6MuSDsu2nULFxsjLXGBt74eWfu8EwMxQbCsFHU4fZ6Lo m93MgzA6jofU6FQbDedF/nZnfvvlll53+dnUIpdfasQ+TZdYghyd7NQ1m+C/Yf+XEYLT HoRA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIQO2cnuHHkZBNASqK3Bh6x5bSD2+8LJ/NDWSQ2uU5LZPAYeqj1 Uwy2piNMaUXhpvs7ZorAQ3U= X-Google-Smtp-Source: AJdET5c12C9ENupQ5aU/5Roi2I51AvBFHA2q/zPzZm1Bni19Z1Hu/WSHNiv0plC1S/FMCpbQ3m61Dg== X-Received: by 2002:a9d:5ad:: with SMTP id 42mr46633otd.0.1542320803619; Thu, 15 Nov 2018 14:26:43 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2c62:: with SMTP id f89ls7872279otb.2.gmail; Thu, 15 Nov 2018 14:26:43 -0800 (PST) X-Received: by 2002:a9d:2c22:: with SMTP id f31mr46827otb.4.1542320802976; Thu, 15 Nov 2018 14:26:42 -0800 (PST) Date: Thu, 15 Nov 2018 14:26:42 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <522f566c-54db-4a23-8cfe-1a2d1e9dd697@googlegroups.com> In-Reply-To: References: <0090c5e9-8e11-484c-953c-bf2958d03b72@googlegroups.com> <0472bc2b-0212-48b9-bfe7-fb98c7916763@googlegroups.com> <5b276491-e7b8-442a-b76a-d395f8e916a6@googlegroups.com> <246b6c0d-39c6-4279-8149-40d1129047fc@googlegroups.com> <1c1cd0d1-47d2-4067-a8c8-69104150f528@googlegroups.com> Subject: Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_831_2085961209.1542320802171" 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_831_2085961209.1542320802171 Content-Type: multipart/alternative; boundary="----=_Part_832_587934820.1542320802171" ------=_Part_832_587934820.1542320802171 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thursday, 15 November 2018 19:30:08 UTC, Michael Shulman wrote: > > However, this sub-universe coinciding with the modal reflection of the=20 > whole universe seems to be something very special about open=20 > modalities.=20 > We may consider the dual question of whether =CE=A3 is an embedding: s : (P =E2=86=92 =F0=9D=93=A4) =E2=86=92 =F0=9D=93=A4 s =3D =CE=A3 This is again a section of the same retraction r : =F0=9D=93=A4 =E2=86=92 (= P =E2=86=92 =F0=9D=93=A4) defined by r X p =3D X. This time we have that the idempotent s =E2=88=98 r satisfies s (r X) =3D P =C3=97 X definitionally. So consider the projection =CE=BA : (X : =F0=9D=93=A4) =E2=86=92 s (r X) = =E2=86=92 X and the sub-universe determined by this co-modal operator P =C3=97 (-): C :=3D =CE=A3 \(X : =F0=9D=93=A4) =E2=86=92 is-equiv (=CE=BA X) Then again we have a definitional factorization of s as (P =E2=86=92 =F0=9D=93=A4) =E2=89=83 C =E2=86=AA =F0=9D=93=A4, where the embedding is the projection, showing that s =3D =CE=A3 is an embedding too, and that M =E2=89=83 C, even though the fixed points of P = =E2=86=92 (-) and P =C3=97 (-) are quite different if e.g. P =3D =F0=9D=9F=98. So the subuniverse of P =C3=97 (-) - co-modal types coincides with the P =E2=86=92 (-) - modal reflection of the universe. (I coded this in Agda to be sure this is not an evening mirage, available at the same place. The proof was produced by copy and paste of the previous one, with very few modifications.) 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_832_587934820.1542320802171 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Thursday, 15 November 2018 19:30:08 UTC, Michae= l Shulman wrote:
However, this= sub-universe coinciding with the modal reflection of the
whole universe seems to be something very special about open
modalities.

We may consider the dual question of w= hether =CE=A3 is an embedding:

=C2=A0s : (P =E2=86= =92 =F0=9D=93=A4) =E2=86=92 =F0=9D=93=A4
=C2=A0s =3D =CE=A3
=

This is again a section of the same retraction r : =F0= =9D=93=A4 =E2=86=92 (P =E2=86=92 =F0=9D=93=A4) defined
by

=C2=A0r X p =3D X.

This time= we have that the idempotent s =E2=88=98 r satisfies

=C2=A0s (r X) =3D P =C3=97 X

definitionally.

So consider the projection =CE=BA : (X : =F0=9D=93= =A4) =E2=86=92 s (r X) =E2=86=92 X
and the sub-universe determine= d by this co-modal operator P =C3=97 (-):

=C2=A0C = :=3D =CE=A3 \(X : =F0=9D=93=A4) =E2=86=92 is-equiv (=CE=BA X)
Then again we have a definitional factorization of s as

=C2=A0(P =E2=86=92 =F0=9D=93=A4) =E2=89=83 C =E2=86=AA = =F0=9D=93=A4,

where the embedding is the projectio= n, showing that s =3D =CE=A3 is an
embedding too, and that M =E2= =89=83 C, even though the fixed points of P =E2=86=92 (-)
and P = =C3=97 (-) are quite different if e.g. P =3D =F0=9D=9F=98.

So the subuniverse of P =C3=97 (-) - co-modal types coincides with= the
P =E2=86=92 (-) - modal reflection of the universe.

(I coded this in Agda to be sure this is not an evening mi= rage,
available at the same place. The proof was produced by copy= and paste
of the previous one, with very few modifications.)

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_832_587934820.1542320802171-- ------=_Part_831_2085961209.1542320802171--