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-x23a.google.com (mail-oi1-x23a.google.com [IPv6:2607:f8b0:4864:20::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 117ba88d for ; Thu, 15 Nov 2018 19:23:23 +0000 (UTC) Received: by mail-oi1-x23a.google.com with SMTP id n10-v6sf12097542oib.5 for ; Thu, 15 Nov 2018 11:23:23 -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=6Dn0x3Xu/oRGi31c62iCKB7zUsAgTlXo5mpyWnv+5i8=; b=C+Jok7ACYainiJjjOx1W1KA9TA7coexz2/A6UVi5ygQguqUMYhzcABYNLkJ9Xd4rhm hdLYvL8FCy9SX3ToWvdkf9I8Qzk7SqjS9nXjdici0Kz2vW6YgzyA5UNjwYltIusM1myD HfksxvXTKYY7ZpOdCgPKBVp3GrGFS21msvTaPYubbsQhT0VgU0xmTHFi1DWb8axMrRJn XE1GtR72rBUW6YlJjUvWR06Xe6d6SchwKsJ//2BY++jZbH96ZMvsArx172vpehBR0F4q iJdZk7BkGE370+Zo/LGARB60ZwI8e1KTpuFnA0p3JmujoOBnHc4PbYv8bNPAuBxmhHSv 8sGA== 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=6Dn0x3Xu/oRGi31c62iCKB7zUsAgTlXo5mpyWnv+5i8=; b=i116T+/NO0p6tt7Ip70A5ITNtvAguuJMaxDIQqpmPHj2uvTQLnNNwhjqDyvYudMAot JcVvSS/8xTlxBjYb+maSo/U93pgHUDiUlHq1660o5BKaB9yulPm3EXRaVvQ29Bar7/hs nYnU/yOqsg+HuHFhBVw0BEtfcr3x1BtckTmGXzdWppWeSeOZcdtcOPp2RAYWYaghJc3B tf4HLmN7NwBoRnlKOg73K8m09lxnqrLKwyv+MM+/4SUWZBdJvIgHVUPFeI7TasSzSICq Fga5NAuDtTMIFop74V8A/n6WIczhBoz0uDpl9aOsWPZQ1z4YpuduMwJPbIL73GdatlSK i4pQ== 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=6Dn0x3Xu/oRGi31c62iCKB7zUsAgTlXo5mpyWnv+5i8=; b=UYMvWj2oGuxwTouXTlo+lemqYejf6GKP1pYU2j9zWgy7Jk/JsHyHRivkDp9HdKt5f8 CW9/eeJB0c/+vGPQyhMfpdHxu7ra5jWFODJaFYNDNynKZ1v8sIfJ5zLRNaFzzLiPYzWe y0NfvpfjXs5bQi1rpIOCzAWcZRDR8wnZAobL+JtrWf9kTHH32sBEW6Os7BARYiNEArhi 130lIxT7BKJ196+9vqxnd6a7CNZDCz1rGexKYW+dnDumpNz6R0thONoja0GBLwftsaBT sFlnoDj6TTxQMHsaDUX8ZGLw9lb0T4Bn2A4cESnp5QxUkJpcag837IXcB2N+g86lX89G x1fw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLzsD4+jYddbOxup5qQzsRksGSC8Bm7KXaBkDTDgAz87cmvyxtr 8wjPIIWRv6w0OPA6rDcUe8Y= X-Google-Smtp-Source: AJdET5fUgYY2x+3L4bFaJG6f45QNT7p/z1L2dDceLcSqsWz4YStmvKaFZHAjaCM7IQmkuUaDKWwxCw== X-Received: by 2002:a9d:24c3:: with SMTP id z61mr35292ota.1.1542309802041; Thu, 15 Nov 2018 11:23:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2ba9:: with SMTP id u38ls9780391ota.9.gmail; Thu, 15 Nov 2018 11:23:21 -0800 (PST) X-Received: by 2002:a9d:5403:: with SMTP id j3mr36720oth.2.1542309801373; Thu, 15 Nov 2018 11:23:21 -0800 (PST) Date: Thu, 15 Nov 2018 11:23:20 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <1c1cd0d1-47d2-4067-a8c8-69104150f528@googlegroups.com> In-Reply-To: <246b6c0d-39c6-4279-8149-40d1129047fc@googlegroups.com> 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> Subject: Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_702_232297086.1542309800608" 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_702_232297086.1542309800608 Content-Type: multipart/alternative; boundary="----=_Part_703_1429342821.1542309800608" ------=_Part_703_1429342821.1542309800608 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thursday, 15 November 2018 11:05:42 UTC, Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 wrote: > > > (P =E2=86=92 =F0=9D=93=A4) =E2=89=83 M > > We take M :=3D =CE=A3 (X : =F0=9D=93=A4), is-equiv (=CE=BA X), > where the function =CE=BA X : X =E2=86=92 (P =E2=86=92 X) is defined by = =CE=BA x p =3D x > I think something interesting is happening here. We have the "open"=20 modality =20 P =E2=86=92 (-), and the sub-universe M of modal types coincides with the m= odal reflection P =E2=86=92 =F0=9D=93=A4 of the universe =F0=9D=93=A4. In parti= cular, this means that the=20 sub-universe of modal types is itself a modal type. Has this kind of thing= =20 been observed before, for this modality and possibly the classes of modalities= =20 already considered in the literature? 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_703_1429342821.1542309800608 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Thursday, 15 November 2018 11:05:42 UTC, Mart= =C3=ADn H=C3=B6tzel Escard=C3=B3 wrote:

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

We take M :=3D =CE=A3 (X= : =F0=9D=93=A4), is-equiv (=CE=BA X),
where the function =CE=BA = X : X =E2=86=92 (P =E2=86=92 X) is defined by =CE=BA x p =3D x
<= /blockquote>

I think something interesting is happening = here. We have the "open" modality=C2=A0=C2=A0
P =E2=86= =92 (-), and the sub-universe M of modal types coincides with the modal
reflection=C2=A0 P =E2=86=92 =F0=9D=93=A4 of the universe =F0=9D=93= =A4. In particular, this means that the=C2=A0
sub-universe of mod= al types is itself a modal type. Has this kind of thing been
obse= rved before, for this modality and possibly the classes of modalities=C2=A0=
already considered in the literature?

M= artin

--
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_703_1429342821.1542309800608-- ------=_Part_702_232297086.1542309800608--