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=-1.2 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yb1-xb3a.google.com (mail-yb1-xb3a.google.com [IPv6:2607:f8b0:4864:20::b3a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 70bf4817 for ; Thu, 15 Nov 2018 23:38:30 +0000 (UTC) Received: by mail-yb1-xb3a.google.com with SMTP id x12-v6sf16064244ybp.9 for ; Thu, 15 Nov 2018 15:38:29 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1542325109; cv=pass; d=google.com; s=arc-20160816; b=SWYC732yL+T/0ceYdYG+tMUFbg4Cxp/1G9qGrcO0cKXpoUMB/8bR/V8wmX0RKxS12q aack9HzDsUCqtxPLtrt2DqKlBslpHyOUFs+3Xg7jlaeNM1MDXSsZZZzdodCQL8XBGgya MAuJnKlPK0InGC+Ym+txLI6cnuJMmiH1LcPX4t6B/djjQ1dR5wz8jZmoaeFHWvY17so4 fETZ1OSSNB0PXfzdBjKritDWK3okfsT4Kwsj5xJMvnzWvxh+7KUX/kn3XSAc9R4C4PeL PLpQeN+izNBbqYhwAxwLcoHK4dwnb4C2iCLJIiCTDA206VrJChfEWnIvya7bNgCWXRWz KGmw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=ktNMg+SpTQPgzOeScYvdZGM+TKybfuMkQ5OckL7udio=; b=mVMTaK7fUniJyi/+nm61CmHiD2QisMZe8WO9KSycuMz5pcAKmrtqGdd+rByJtU2u2j 0r5Ai0D9tAwOQu9Y+mN9aEIZFA7YL3J0vx6GvVGt/Zi9HJEjgWoaAXcIy4PNmXWDBCKB sb6y8vS1jFYhL1c6noZ5+FeHmHU8rZ3sm3FMGYroLqcc+2EF2C6V7ZRUJUXd/MRpX6/6 S/SuEGKjehokIVduFzIqOBqCmjWSbv3JLIQuFCnPIFbPr3JXVBTs/oe9c3wB8MRw63r3 d8rhieI0un1kAsqi7rzw7uLx2tpscZ7lb5p1b41MKz+HyU6sQe9IToYietTEFI9pBFbC GJNQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=L+JvMABT; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=ktNMg+SpTQPgzOeScYvdZGM+TKybfuMkQ5OckL7udio=; b=dA9x25F3TmhgNJN9Y2nsNx20PwYiv18O7ykBAGIgBK69do7efPS71KWVArWveOJmHg ocfjWxxluyxH1Uh0BA9HjV4UKYVn2S4ugnnxrNAiTNTQwX51vB6P5xccOj9wiKb2EmkM kbO57iRrr7ZVIWq1+fP6P9La7NKl90r0IvNzo+6YTk576bLFBF1lG441S3BOTVUQ4J8t ahVCMdEpU2o5pLL03WZI1cXHc90gKu3VKonVLE+i2g2g4NBbNdNG+ruuq+WDj1nxRIU1 8ImAgV744lsLl1C2Y0JhoATUSIB/cJnzFj8/7fTevlLzAb0me9Ivo5wqm3eVMzNEW3LK Iumg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=ktNMg+SpTQPgzOeScYvdZGM+TKybfuMkQ5OckL7udio=; b=FCcJaLtbVVVqdA0J8v+DsQLkmzzJchJ9eOESxPwEpJe4Eaz1dj+xs9hjwB3ea6Ibgl 4AiHNpPZ98VSnNq9KVScIWlR6Mq0q6J+XPVgVELTayaUdhAqB6jbrVTWBT847bKBYNuW NEAo94YAloPYjJsAh9znRuCw3r/JhSHFhv+YFaLyRk9uA4gT5W7rJkU6bf4O4YDQB7OI NKU0/bkyod+nlTHHTrwBvyZ4tKJ38wf4dZ6Xmicv3uyMW0MU5Ntio0V17ySGwfbpvwTu t9D7WlDRo1l8JWeS0wKRhcqjIv4WWx5VSnyZUQw0wUFW4qSq1ensw8RWLI8tYEwyf3/z NC6Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIox8wCKQ55pcDAtBDw+ERrGn5KCVgBg8BzSxu5GUmmOVmpXFYV CSvFK5DZz8ptDeWM5ttKueY= X-Google-Smtp-Source: AJdET5eEJTdprecylrHA1t5yhlJ/8ytlO9p+6zF0S89VuV9rAqK8ufMz51gthDH65hdML1GpvRqCeQ== X-Received: by 2002:a81:27cd:: with SMTP id n196mr22614ywn.2.1542325108930; Thu, 15 Nov 2018 15:38:28 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:180b:: with SMTP id 11-v6ls5355296yby.11.gmail; Thu, 15 Nov 2018 15:38:28 -0800 (PST) X-Received: by 2002:a25:dbcb:: with SMTP id g194-v6mr1276815ybf.95.1542325108610; Thu, 15 Nov 2018 15:38:28 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1542325108; cv=none; d=google.com; s=arc-20160816; b=WEnh2/TloBb4JBlAUmfreQ8e0+Zbn7UbxtEugd/QE5ZwueR/F4Ui4JjU8LJ9l7/2s0 nMwyIEsU+HU6JoACw9RIe0lYQQOpCmILKU256pwrUVBknnIqbiRVd4fLXm8yQfTohsSx SlAy/cR5LyVSUaguiFltRywI8BduiCJt7A3kAdxzHGzYf4CO3RH54D7/4eRgScEOWskT cKyHUx8WoHKK0pSQ+IJSy0EOK82IYYNt3Y2m7XkSs8Lm6Q2FXo12bsWx2FtIO58NsttT JKE/zRqUryNl8FVzw3NeZVyHzJsjIwAYDFRO69OSX4mqqPW6nh6uGzHa+9sWPOoA3Ij2 Q1Lw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=ZqYJR3HAPOJ6Hxrh7Ko6z9qns4TfDrGEhjo9UtnGwOQ=; b=qrVaxJvCUSahcmiCB0iF0rXDVyR70pnOy8H5pnacnQubmWJV8NKssBg2M0arPduOKl 4bn9ySzcRdH68ny0EKXSxHa9XI+d3jxZzKajij7OC28/8zfKWNWqRKNem1iAhMmVrvGn MOtuv3XrCn90MbPjsumHXS0XSM+xWmz0kQH+C1jiHgtql3S3JQzUpSblNB1tdwNlpVbw +7rQDF85qeYv/hwaUAo5xdZYhV01JxM/3u2xhXI7hCste2Swm1aypo4DWDfvscTxN603 dC/wiuNBKWdlaIMBDcj8jT6eUCq3EK/TcCP7dKgNDWXTIpQ8CivK6g9h+OmnebUlXPer CPsw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=L+JvMABT; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc34.google.com (mail-yw1-xc34.google.com. [2607:f8b0:4864:20::c34]) by gmr-mx.google.com with ESMTPS id l125-v6si1200935ybc.1.2018.11.15.15.38.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 15 Nov 2018 15:38:28 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) client-ip=2607:f8b0:4864:20::c34; Received: by mail-yw1-xc34.google.com with SMTP id z72-v6so9463379ywa.0 for ; Thu, 15 Nov 2018 15:38:28 -0800 (PST) X-Received: by 2002:a81:62c6:: with SMTP id w189-v6mr8097253ywb.38.1542325108169; Thu, 15 Nov 2018 15:38:28 -0800 (PST) Received: from mail-yb1-f174.google.com (mail-yb1-f174.google.com. [209.85.219.174]) by smtp.gmail.com with ESMTPSA id c140sm8133457ywa.74.2018.11.15.15.38.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 15 Nov 2018 15:38:27 -0800 (PST) Received: by mail-yb1-f174.google.com with SMTP id 131-v6so9067552ybe.12 for ; Thu, 15 Nov 2018 15:38:27 -0800 (PST) X-Received: by 2002:a25:704:: with SMTP id 4-v6mr7819149ybh.115.1542325106974; Thu, 15 Nov 2018 15:38:26 -0800 (PST) MIME-Version: 1.0 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> <522f566c-54db-4a23-8cfe-1a2d1e9dd697@googlegroups.com> In-Reply-To: <522f566c-54db-4a23-8cfe-1a2d1e9dd697@googlegroups.com> From: Michael Shulman Date: Thu, 15 Nov 2018 15:38:13 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle? To: Martin Hotzel Escardo Cc: HomotopyTypeTheory@googlegroups.com Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=L+JvMABT; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , I remember noticing before that the P x (-) co-modal types coincide with the P -> (-) modal ones. In topos-theoretic language, these common sub-universes are the slice category E/P, which is related to E by an essential geometric embedding, hence an adjoint triple i_! -| i^* -| i_* in which both i_! and i_* are fully faithful. The left adjoint i_! embeds E/P as the P x (-) co-modal types, while the right adjoint i_* embeds it as the P -> (-) modal ones. On Thu, Nov 15, 2018 at 2:26 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > > > > On Thursday, 15 November 2018 19:30:08 UTC, Michael 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 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 > > -- > 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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. --=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.