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-yw1-xc3f.google.com (mail-yw1-xc3f.google.com [IPv6:2607:f8b0:4864:20::c3f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7db615ca for ; Thu, 15 Nov 2018 19:30:09 +0000 (UTC) Received: by mail-yw1-xc3f.google.com with SMTP id l11-v6sf15542086ywl.16 for ; Thu, 15 Nov 2018 11:30:08 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1542310208; cv=pass; d=google.com; s=arc-20160816; b=JoMHn4Q1T2bHToKwXgHyU9JOR+7fTJp+jLkERqgqY6LqXnJ0dtSYH4sKl4n+fjQpSa W/RWeJQGfyOzE2SAkxbjlHK7ES+rJYwMIsHPDCCv6UjDFcn7J+tU/JOwQNaq9T6qUVkE q8thsH/d9YMxiyOoCUmpSH+Dh0A4cOEgLNJ9XZThUZRCKBQXACp7CTM4AncjhzY8vHgH 6XrM/16XE6FAOioTxPzW2hAOhycps3UvR+oACIl25GbfVq4T6kW34N0FuRJDRjkvSJKi Tb0YSYQg332V8XLypFLo5gLpa3lPxk+k9JTfv5aZ9CgSDy43gO33ko9kKD23ZfH8cTQK LFCw== 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=kiLkHgU0NoPZaSBP3IwlsGeBJHlVDyoRB+v9Hx+mdDQ=; b=XTg67rCJAeERwq/bUHkr2GgMyejYtKpmKQxAEn2BLG9Jg4cU8fXo9hXRQKZFuY1Sie usLkBFWnBbmVzb5nlhX1uAQAkjKdjbF1FtZ555N5RF0cNoUGXo5PwyS7q+mvfuZbcfef HtP6iIy5g4Pc4QHDYUbuIQoDcfwgzyIDiEv5I849ci4S7BdsAt1yaaRVfYcZ8VgKJnWL LjDHWUDCj4pVT04N0CFXIjtXR321xaApj+xKecXPpqh9Dxh/C4GiEKkLL7p00XpDvOye Fcppsr4PKgXUpDxfFJCe/r8UeBHb7KntOxu9VgcK4pJ2Q4ZBajW+Z+OT5wRshSKso5cY evPg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ESjh9rOD; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b44 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=kiLkHgU0NoPZaSBP3IwlsGeBJHlVDyoRB+v9Hx+mdDQ=; b=PgbpCSrO/0bgAp4+5DTh+ppISSN6J70RF+Oa7v8xlCE6cAAx62MUej+Ih9soI2h3fa XybkwskWLVlynS2dq/5/bC6er9ip3Cm5Wxxk03w/haQz6I1YtzX4uv1gYiGFd1tGVsM3 0bqxiQK0NHh92B3dyVAuVoPAe/F2jK5OYeUGAaWVAthBPd3sJ9GroVgoP8pwauup8jZP IkLFmO2AQBdqcdY+dBNpotJtzbpLbtRs7jvIOBnvMDWfIgq+E5Yh5TeNRgQnBQZMlvdm +DArI6u1MeWRnOF2yhbNvaWOKl+NoJHjJFFZYyPr7NWX9j5SSJuUreQnNiRfkjYy243i EuuA== 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=kiLkHgU0NoPZaSBP3IwlsGeBJHlVDyoRB+v9Hx+mdDQ=; b=QcVEWlMKSlel5gj9dTYqEitXJG6EEzpOAlP3yhVhYoIFVPDEiZ2JZd55PvP8aYAOxQ F1v7SjxzbsjvhpsAxAPiQdgoK3mkfzgG89o8kUV96jayKNj6g0Z63zV1oGonC+0J4/lx SEAcCJk4jeyFCiHcQtpVCj+O2uYSStQNA8txqwQxy4DU2Hrb+Q9VltYnVRnVcT/7qTkh r49NR38mNVWJlLotlEIAI4gm5LsaZmtrh5YBHZE6Viw7BxpI5LMYL9/6Rr5UINDsYZVE EIQfKBxbK9PUwF5Yw2mpir0EvkUHmpAalVuQnUSeL7KqniK7BAXse5zWReeo61eRFc9m l0zw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJXWmnLp/6ADX3b3Hgn6VrnT2MUt4CwzpsAf3bOSp2LvAN811BR pIvylSZMhdoRr+eqG48I7Rw= X-Google-Smtp-Source: AJdET5cSNtBWoPJTyMg2nQmBFKlMawb2lnrfwNV3RlwvZP875H3Yh3gWGnrnKod/0vQCdp6nERzSSA== X-Received: by 2002:a25:ab52:: with SMTP id u76-v6mr17035ybi.1.1542310207949; Thu, 15 Nov 2018 11:30:07 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:1057:: with SMTP id 84ls7949725ybq.14.gmail; Thu, 15 Nov 2018 11:30:07 -0800 (PST) X-Received: by 2002:a25:ef47:: with SMTP id w7-v6mr859741ybm.58.1542310207694; Thu, 15 Nov 2018 11:30:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1542310207; cv=none; d=google.com; s=arc-20160816; b=hy7j/7kHrRgLZFAnmZBjmDqwbVJztlJoyuCpqw09+K+Y1fiPQlpY/6t1SBYHZiw0vC jJi5C7w1gxKxRNFkmk/25M/rhk1pHjbngTwXuQ2wMolw+sFRpp7RBIcVDXfqsbbMtb8C mo1ezmzXn10iRiTs59XV3CDf3v3ypnOdrISU8+KS543h1VMfG1hKK634DMuaxRrUEhWM P6rfoXqzni6MUDwIOsTLY+cAYHQB0jubrZSLuosRMTF4lTZOC54l9d4p4MZ5j135QRl5 RoTZz1DRp8NqYIrHHFHDVoKmAMOdrNlTaS63sc+D1uX3BSRhNBhc2hzuddP11k+fEmQ0 ULvA== 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=DczNhksfAAYKALSFNMwHgDcMu5T29pwZdiPv6ARYLAQ=; b=senNyP+nIIZANvJMAbZ0SHOu0CM5zh4TGjUtfsAOCgx4L3KivfHoA9Cg3CXi96H64c 3GO4FAEUG4d5RbRMCUSSAIEGq66lUSMfNlDSUrkyjH+TahjHvFg6B3ddZUMSsPMODNZq vug6d+23j5mNkXKXI6k9uQTw95v1i6r3YIxlOJfnTpmRCqdWfeS6CuG63w5xXGXUmy1I ORDMaksgrhbaQPCyzmeTwBIlxsD+CgR+gmKlzJvsO8ApRmmjKhxoEbrQaqRemUK//Hzp 1qybxQ6Zs4Np6t5jJdcTuCFLmhcnWWHl399ybHflEJFc+pwHetzbvUdgH9es9bEM8+B3 zFWg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ESjh9rOD; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b44 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb44.google.com (mail-yb1-xb44.google.com. [2607:f8b0:4864:20::b44]) by gmr-mx.google.com with ESMTPS id 192-v6si1134222ybv.0.2018.11.15.11.30.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 15 Nov 2018 11:30:07 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b44 as permitted sender) client-ip=2607:f8b0:4864:20::b44; Received: by mail-yb1-xb44.google.com with SMTP id g9-v6so8817331ybh.7 for ; Thu, 15 Nov 2018 11:30:07 -0800 (PST) X-Received: by 2002:a25:c145:: with SMTP id r66-v6mr7184960ybf.93.1542310207308; Thu, 15 Nov 2018 11:30:07 -0800 (PST) Received: from mail-yw1-f44.google.com (mail-yw1-f44.google.com. [209.85.161.44]) by smtp.gmail.com with ESMTPSA id 123-v6sm7057653ywx.15.2018.11.15.11.30.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 15 Nov 2018 11:30:06 -0800 (PST) Received: by mail-yw1-f44.google.com with SMTP id r199so1491401ywe.4 for ; Thu, 15 Nov 2018 11:30:06 -0800 (PST) X-Received: by 2002:a81:4d42:: with SMTP id a63mr6949932ywb.189.1542310206075; Thu, 15 Nov 2018 11:30:06 -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> In-Reply-To: <1c1cd0d1-47d2-4067-a8c8-69104150f528@googlegroups.com> From: Michael Shulman Date: Thu, 15 Nov 2018 11:29:53 -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=ESjh9rOD; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b44 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: , Modulo some details about accessibility, the sub-universe of modal types is a modal type if and only if the modality is left exact. This is theorem 3.10 of RSS https://arxiv.org/abs/1706.07526. However, this sub-universe coinciding with the modal reflection of the whole universe seems to be something very special about open modalities. On Thu, Nov 15, 2018 at 11:23 AM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > > > > On Thursday, 15 November 2018 11:05:42 UTC, Mart=C3=ADn H=C3=B6tzel Escar= d=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" modal= ity > P =E2=86=92 (-), and the sub-universe M of modal types coincides with the= modal > reflection P =E2=86=92 =F0=9D=93=A4 of the universe =F0=9D=93=A4. In par= ticular, this means that the > sub-universe of modal types is itself a modal type. Has this kind of thin= g been > observed before, for this modality and possibly the classes of modalities > already considered in the literature? > > 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.