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-pg1-x53d.google.com (mail-pg1-x53d.google.com [IPv6:2607:f8b0:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ca765a7b for ; Wed, 14 Nov 2018 15:52:46 +0000 (UTC) Received: by mail-pg1-x53d.google.com with SMTP id r16-v6sf10803266pgv.17 for ; Wed, 14 Nov 2018 07:52:45 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1542210765; cv=pass; d=google.com; s=arc-20160816; b=HeqIIzfM1aaom4c0bY0TmRZU4uJ1s4NpiPjnpxxvTwWP5TFoT8EZebHQ1ldS0gOsUa AsYWn3AygwPcGNiZeV6qoGjhbkITsMM6AmtzngaWaTg8M3BC9ks5CFXJKF2ejxltFI1n qfc5vg5YdeJdHisnrDa0uhhKgVuO+nOfiHaICyV+2YhYjHUVkewN2psvgsu/0PtTeyI+ lIgcTihQ4mrVBfCU3uyzdlpWYa+mekjFdya1Tp7ItUoxYmOetUx7eHzYC4W5mNtfqFct IJXjojaR0r+M4jUGxYKu6f42/q3+dtAXiaJZLlXzhbXbVbZdI9ZknW12jIu/WfAZITn3 8w+w== 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=haT1J9r15NUiDwDNNFI6579i9hRtdDt7FfSmjlLFkGc=; b=lrae1exFzg/DixfO/rP4LO/KyE+OVx14f0CBnfhmbDkx1IbowrZCa2ndPT6M7/TtZN +2H8EQ1kdy9G7RhWMjdL3EstlN5oSVJpPbbZHXSM58Jk9D3g4S2YNroWFqrpedNzrMCS hMzsG92gnG5B78eY9aKmQTodI5Hwx8u+CLr1hx7BsVN/KjsFMTDnAlbu0vT473JmDeWb gkqVfuCTSq74S2/Lh+EoY2peSRi4TF4ijVKDDr0aPEdu6w6MyWGupIAU8PatNzIV6ctB ub7Ojh5HSDmNzCKztTBh5BnT7VnV8NOlveU8bXB/Q49yyJ1FL5mGumYyTawkQcuAWPvl brwA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ZBKeB+GL; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 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=haT1J9r15NUiDwDNNFI6579i9hRtdDt7FfSmjlLFkGc=; b=Z6w1/u+q2s4ckoKKvSCY6L21fgiU25YiqamQTs8ajCYv1CipovEHdiGqqk8Y3GtLlh CJM18jh3jjBUNYwA39q1EOoEnowYE/SLPK/jchlJ03+onUJFR4eTfIlV9jxogz0qhdBH FG1RSKjWjQfWDrwsdz943I08Fhr0DHR7dMEogGR/ErM/hU1ILwT9KMI3IsHMyRAsLhKZ gyBBDqubArnpB8hELFSZ7HJ3kgy5iKY20GkgHkkePWVWzxdHYND1c9Acdo9lJejwnL3H rHcJB9t0aXQWFUr7FCcSkXRnrO438kdjNUTZZpRqNkQidkUdBI6iuMxYWVMWfowyMHZ5 Ukiw== 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=haT1J9r15NUiDwDNNFI6579i9hRtdDt7FfSmjlLFkGc=; b=h8zOG9o+TzNxGKKBHKpEn//j+qoxpgioSS0sK9ZSjsBkvJDHcVYLtBVeHctZrmAihB 4J7Pn8BW+sFRJDrsz1Co3SvRyxhkfemNl3/vs0ybW4obSIv1eo7S/41ivN8fh5mEXKR/ 9UP4VxJw7c//1kiv1SHDs4F/uexpO6X+Lh/mEvsE/sLxk8r9x9pI6VP/le4dKbng2Fx+ ImNEVXr0YfJz9dLkTuFjrBCKtVSG/2Ga++81xdTt7lDzftlWE1WqzaVGE1YLut6oeamz DEGnprxbz9MwUC9S6a3de2cQsM4SHpib+VE6LogH8ehzeo26/vV0heR6QW6M3ni/bXOp aJwg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKbVugGnsq/GVjDFad+qCSGuMCt1QYRscNOT2ZwrVKyoWxufSvZ dlw7+AgRLs5X/77or7wUgok= X-Google-Smtp-Source: AJdET5f64rGu5vCPJRY9Y9RiCODkw1NUdFsFxQXu+DnkJPtlYS7pqRBgGqcQjeUoThky4zbFUi8KFA== X-Received: by 2002:a62:45cc:: with SMTP id n73mr15182pfi.2.1542210764684; Wed, 14 Nov 2018 07:52:44 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:988c:: with SMTP id s12-v6ls5747470plp.4.gmail; Wed, 14 Nov 2018 07:52:44 -0800 (PST) X-Received: by 2002:a17:902:2bc5:: with SMTP id l63-v6mr849713plb.129.1542210764245; Wed, 14 Nov 2018 07:52:44 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1542210764; cv=none; d=google.com; s=arc-20160816; b=wbkSI1ln5vfEsWviD18vyMB2VsExQj8K4UAmMYYQbExJ63p6yYECU4VKgKjXWDOlgd gjjmvrNogzEtewQFGh9bN6ggJyMzS9erIxmEKg5olkO6R++sXAc44qia6rnraKP02QcI zQF1O2TbBcIFC8Ttk/2vK6muc+RJwtKYV2i1CzCpnTLuTIyM44duj1dmirTbgAe/EKT+ Ipk3qjS+UDqnYfqpH7lDdYOHayC2TVx8qvHDSGbD16ZGESGH2O06K//vxdL0B7aqR9rI dXUUeIVXrX+VSzeEpTo7Yw2h2xsb+qunrVX5km7dJ6raM6pZcA1yWP3cvUV6oP+D+7zb XTNA== 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=/kwhlbD05G+8O85IsfVPqfTSFVHmc2U2rWpd3FllgnY=; b=XIxYZg59RfwKLyeJtiBGxnVb32HvfQBUKSNBHaqjIUZiLwN0cVCztTcRIQldmoI+7b awkK1b24k23N7w33esTHMxBJCob/qVGCckrz0uhpMZl1Us7O334r/tO3DOU/883bBsd7 J5CJ3QlVWR2HSft8X9nfF9SU+WRbznbz1T/ck7+Mbm4BoKDzagGoREmYlyIT4/sgeDb1 0E1svQmM7GL4suiYQ21Cq1x9GYKWAvKfX3a+3X3xJ7W1B0/GLcdJvwrhptpsE9bVV8AL 45UZyNcg//MTtxLsXozcRgEyeZqq17AIhh5ZoYYmBvRgbaV2mwaylvwJ59GlHK12XEmC m0tg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ZBKeB+GL; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc32.google.com (mail-yw1-xc32.google.com. [2607:f8b0:4864:20::c32]) by gmr-mx.google.com with ESMTPS id p4-v6si920867plk.1.2018.11.14.07.52.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 14 Nov 2018 07:52:44 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 as permitted sender) client-ip=2607:f8b0:4864:20::c32; Received: by mail-yw1-xc32.google.com with SMTP id c126-v6so7422642ywd.8 for ; Wed, 14 Nov 2018 07:52:44 -0800 (PST) X-Received: by 2002:a81:af1a:: with SMTP id n26-v6mr2114587ywh.243.1542210763601; Wed, 14 Nov 2018 07:52:43 -0800 (PST) Received: from mail-yb1-f182.google.com (mail-yb1-f182.google.com. [209.85.219.182]) by smtp.gmail.com with ESMTPSA id x206-v6sm7990582ywx.25.2018.11.14.07.52.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 14 Nov 2018 07:52:42 -0800 (PST) Received: by mail-yb1-f182.google.com with SMTP id u103-v6so7073425ybi.5 for ; Wed, 14 Nov 2018 07:52:41 -0800 (PST) X-Received: by 2002:a25:8686:: with SMTP id z6-v6mr2088045ybk.202.1542210761509; Wed, 14 Nov 2018 07:52:41 -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> In-Reply-To: <5b276491-e7b8-442a-b76a-d395f8e916a6@googlegroups.com> From: Michael Shulman Date: Wed, 14 Nov 2018 07:52:30 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle? To: Paolo Capriotti 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=ZBKeB+GL; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 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: , Here's a sketch of a more conceptual argument. Both =F0=9D=93=A4 and P =E2= =86=92 =F0=9D=93=A4 are the object-types of (oo-)categories, and =CE=A0 is the object-map of a right adjoint functor whose counit is an equivalence. Thus, by a standard argument, it is fully faithful, and hence also fully faithful on equivalences (which, by univalence, are the equalities). Of course we can't define the whole oo-categories in Book HoTT, but I think this is one of those arguments that only needs the 1- or 2-dimensional structure. On Wed, Nov 14, 2018 at 3:07 AM Paolo Capriotti wro= te: > > On Tue, 13 Nov 2018, at 8:32 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wro= te: > > Let P be a subsingleton and =F0=9D=93=A4 be a universe, and consider th= e > > 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 *n= ot* 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)? > > I think one can show that ap =CE=A0 is an equivalence by giving an invers= e. Given X, Y : P =E2=86=92 =F0=9D=93=A4, first note that the equality type= X =3D Y is equivalent by function extensionality to (u : P) =E2=86=92 X u = =3D Y u. Since one can prove easily that (u : P) =E2=86=92 X u =3D =CE=A0 X= , it follows that X =3D Y is equivalent to P =E2=86=92 =CE=A0 X =3D =CE=A0 = Y. Hence we get a map =CF=89 : =CE=A0 X =3D =CE=A0 Y =E2=86=92 X =3D Y. To = show that it is indeed an inverse of ap =CE=A0, start with some =CE=B1 : = =CE=A0 X =3D =CE=A0 Y. By following the construction above, we get that ap = =CE=A0 (=CF=89 =CE=B1) maps a function h : =CE=A0 X to =CE=BB u . =CE=B1 (= =CE=BB v . tr^X [u,v] (h u)) u, where [u,v] : u =3D v is given by the fact = that P is a proposition. Now, within the assumption u : P, the =CE=BB expre= ssion in brackets is equal to h itself, hence ap =CE=A0 (=CF=89 =CE=B1) =3D= =CE=B1. The other composition is easier, since it can just be checked on r= eflexivity. > > Best, > Paolo > > -- > 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.