From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCAPPKFHBUIP7H7E3MCRUBDE5KME4@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,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.1 Received: from mail-ed1-x53a.google.com (mail-ed1-x53a.google.com [IPv6:2a00:1450:4864:20::53a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e260e1d1 for ; Sun, 19 Aug 2018 06:36:48 +0000 (UTC) Received: by mail-ed1-x53a.google.com with SMTP id r25-v6sf1184481edc.7 for ; Sat, 18 Aug 2018 23:36:48 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1534660608; cv=pass; d=google.com; s=arc-20160816; b=YwuJOeLIyi7+p8AdOZrcNkgln3JUdut7z6xY/80kIGmipPbnrgHWwc82x1oESLIXbT y3GeHm2T486tveSJRMvaThWyCPAD6dxUO1hMjCxT6UXEJ4+ZnKFhBmrRZ7fcqI/ltBPf IqEH/8DQPlYbkupL7ZOpsL9JtL0MNkgANiKXYe9yBDpx95dVBhpcLSsOm4OTbuFHIb+Z +KyC55clsPzNPghx+iVtSd1Cs16PvBkoME9UW1crAYnhyJkMogkLxSLnJdVqdojiz/dF v3Op5ePo8z9P4ih1wL9pRjmDGKaY+QFy/+1wBHT+IGQj7jCErFWnuFTAEFX/iwUTorBZ nuEA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature:dkim-signature :arc-authentication-results; bh=lEdHzWODxC6Z5NNkX5AljPUyw2sslCLWYmkza8E6fJg=; b=Wv/yA1d8xKF5wTT9E5rXymML5v+UXzgHWumW4B86u/9f84AIX6GcK6X7Va7p1MHPvX t56oghaNt7jyw/wxRsPPLr4aOWciz3HIP7eQi10ORLEppUu2btAISbYT8ISDOH+NPejS 1kTjHX9zpH3AW+v0oYQ9p0mYpQm1Kk8pB7W4IFk2LpazihXouRWvn+woO86krRqLr3qt wuREqplGvJMsB1RhtngSxi2xpsVKoL2zUdBXe4h5DNYltMixkOcMQy39St49HmJL5Jq6 mpWmm3uxxZmJv5w1eVvhozC0sw7X7Rg3LXJYx9z2kOURQ9U0skv9WYS7mAj1nW+aQE+S d1Cg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bZ107xN3; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::133 as permitted sender) smtp.mailfrom=guillaume.brunerie@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=lEdHzWODxC6Z5NNkX5AljPUyw2sslCLWYmkza8E6fJg=; b=ZPMiyPEn5TL9av+O0R5k3sRDfVqMhuIkIKLAirQCkDylDK3Wb9h30CvOwWUa3ar76q SLZTLwP4Lb8P0ICiJSuoNBUdF04pjl0S6jwgZfZA90cHcpDxLrdOl90PuB/KG8NHQqL1 tNrBrxF9X2fGBvCDWSjEzdwPDz8pT+DaFPkrv5leCRMprt2ZWdy1gCYr/ALWilUkEuC8 5ai9CxRirB1eLtCgnATRnBWqEDyb1TJGr/OH7Xvn9zrrrD/AddXpY/rGrt5Uz0DpgsN+ qeBXS4IOzKtvPXKuJtfs5JgYPJFUspUXJGVi0nFvD1S3yO+xL2fIs1sL3bQ63cU64s99 dhCQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=lEdHzWODxC6Z5NNkX5AljPUyw2sslCLWYmkza8E6fJg=; b=W22H5m4HtQKFshB5uIxEIiR1tTQKdlUWPdcOEpF5eRTnjcI5PqEG9b5D0TXz8hyW3z 9XPXd/3rAREQ92CVt1z7T5Dr9NWZe+ditGPU5HsK8f+rGXEslffpwwKzum2HZLm8O86u lFgfrmysN/Xui1aRcLsE4YeumbCGBPjuhQIOLzntQpzwnZu4opFsvcjbVRnldYCbqf0q Z42SYxLpD9BoKBev+UJZAnbDFUg9fNI4DgiqFUIKN8F0x+QmZxjOHL/p28ea1okE1+jb F9Qr0qZ9ea1gX31aECbNnuC5mI5b8STnIMPRhO5h+R2SL+gY9+sxDrD6SoO1o3o8HL3w +UCA== 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: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=lEdHzWODxC6Z5NNkX5AljPUyw2sslCLWYmkza8E6fJg=; b=p/p9efW0UW7Zqx8PrCmOKOKrThC/ik0OCpB0xwp92g7PvoMovWBkKO54x0zkcOVa+n eFgYeF0AawxeGU0ePxBY+QUf+yyTc19nKDVxS1ZOZTmHe2oJ+WEfT+pR9l9tXeCKCROH iAtgk6aqAQEPmZwv2utaUF30AKft8m2au+qqMRwV1z+k8ZxypqXlW5kQy5lNIYnwFSNQ 0EVnpqagp+ZjF1JadrtqUqaLMdo3rQXsE1Hsk218X4pxiwPtEdw9EUw61/5oVNo2nxP/ ITitdKjvyLB7lL4EAcwYPqTk+mTkcTarHEkpy/pTQuc2TO1WYNJRPbbwk5Ve+7NXPfEY SZcA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlEXwkIgSpdiHNTVYn2DUUU1WdDodCDOx1t1Xnw3TY7poSeCx6vo bnBwo+NCT43XXZP0uB5Jel4= X-Google-Smtp-Source: AA+uWPxC+EQyplBYxhrtxGfAhQ0QPJ03rMRVi5Aw8RGYtOurmv/gxaEZLsdIfFwGAf9LR8DvrO6rjw== X-Received: by 2002:a50:fb12:: with SMTP id d18-v6mr240105edq.3.1534660607271; Sat, 18 Aug 2018 23:36:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:f5e3:: with SMTP id x32-v6ls1255730edm.0.gmail; Sat, 18 Aug 2018 23:36:46 -0700 (PDT) X-Received: by 2002:aa7:c510:: with SMTP id o16-v6mr10787126edq.7.1534660606677; Sat, 18 Aug 2018 23:36:46 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1534660606; cv=none; d=google.com; s=arc-20160816; b=KakQOncB/bGh5KG2wGKPv33e/wBCtk5z1/aToSv27J1AiALTrBtQI23vLhQCGgHkLx WCXuYUDefnn2Jep8VAVVx4OeIwk0ifyVjMjgN+/0Fdn1LdwL2UMrR02Lp9dThuTFPdLF Vb4nDe8wTBeLEOg3QTBB9L5S9P8LMlINfLIWeXaRnkTZ4Sny+5eDHkYfD7k9qO3Oh2Lh RhQGSpmrZ4Sm7+Dbt1jJE58dPwCC8KJCWl9q0Qllu9F9t2zpJVNehWV1H43MU1y2ZITP nbgU+alyWyGQIo2MwEg/7OmaE1Ks7txtdcZ8TdwS84SDZ+DntDqLKqlxZv9APBiZ2BbY UWtA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=osp9KeXfnHLSY75O9RiIaQj1wx5g2qqmtwA4HHC/Vl4=; b=nyn+OppDnfmk7zkjmTKU6vmnAYqMLue/J/Z5SxH0wMI4DomFBD+XrmkW6cTCvfYqLn JV5mR1neatOxPuX8NJ8gwsRkauKGVBDiloKJCGLd2cVpmzaPV27B7SsVSb12ys6VpjqY tgpMKvJcW4JPc4gLDQgaNpC8JKrSKYY7ZznAPxJ9rdgGY4yQfT2AklSKWk+Zz97mzKux YuVSadCExDcX+u22mtzPML0p1DkA/UgY5zi+2Lr+UR8B3IEefDtV3gcps6gPtZKVFXMY bOk2pvep/WVma40eO0SOoczfzHSZeQmYPahXds4PkVuw7a0ulrlddE6h/gMM61jfzzGI H7lg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bZ107xN3; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::133 as permitted sender) smtp.mailfrom=guillaume.brunerie@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x133.google.com (mail-lf1-x133.google.com. [2a00:1450:4864:20::133]) by gmr-mx.google.com with ESMTPS id y4-v6si305165edh.4.2018.08.18.23.36.46 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 18 Aug 2018 23:36:46 -0700 (PDT) Received-SPF: pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::133 as permitted sender) client-ip=2a00:1450:4864:20::133; Received: by mail-lf1-x133.google.com with SMTP id a4-v6so8649239lff.5 for ; Sat, 18 Aug 2018 23:36:46 -0700 (PDT) X-Received: by 2002:a19:cd8c:: with SMTP id d134-v6mr22572056lfg.41.1534660606011; Sat, 18 Aug 2018 23:36:46 -0700 (PDT) MIME-Version: 1.0 References: <874lfrhgwo.fsf@uwo.ca> <87lg93fox9.fsf@uwo.ca> In-Reply-To: <87lg93fox9.fsf@uwo.ca> From: Guillaume Brunerie Date: Sun, 19 Aug 2018 08:36:33 +0200 Message-ID: Subject: Re: [HoTT] Real Projective space (and other projective spaces too) To: Dan Christensen Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000045adf60573c40482" X-Original-Sender: guillaume.brunerie@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bZ107xN3; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::133 as permitted sender) smtp.mailfrom=guillaume.brunerie@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --00000000000045adf60573c40482 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Ah, indeed, I misread the proposed definition. Den l=C3=B6r 18 aug. 2018 21:35Dan Christensen skrev: > The extra identifications are one of the problems, but a more > fundamental problem is that while the north pole has been identified > with the south pole, no other pairs of antipodal points have been > identified. > > Dan > > On Aug 18, 2018, Guillaume Brunerie wrote: > > > As Dan said, this is not a correct definition of RP^n. > > > > More specifically, the issue is that you identified the points "map > south" and "map north" in two different ways: "glue south north" and > > "inv (glue north south)". > > You could try to add another constructor > > glue=C2=B2 : (x y : S^n) -> glue x y =3D inv (glue y x) > > but of course you're now again identifying them in two different ways, > so you've just shifted the problem one dimension up. > > > > Den l=C3=B6r 18 aug. 2018 16:46Dan Christensen skrev: > > > > On Aug 18, 2018, Ali Caglayan wrote: > > > > > This screams to me an alternative definition for =E2=84=9D=E2=84=99= =E2=81=BF (and maybe > =E2=84=82=E2=84=99=E2=81=BF,...) > > > > > > Inductive RP (n:=E2=84=95) :=3D > > > | map : S=E2=81=BF -> RP n > > > | glue : (x y:S=E2=81=B0) -> map(in x) =3D map(in y) > > > > > > Where in : S=E2=81=B0=E2=86=92S=E2=81=BF is the obvious inclusion ma= p. > > > > That HIT would be S^n with four edges attached: two edges connecting > > the north pole to the south pole, and a self-loop at each pole. So > > homotopically it would be S^n wedged with a wedge of four circles. > > > > To get the right space with the right bundle over it, see: > > > > The real projective spaces in homotopy type theory > > Ulrik Buchholtz, Egbert Rijke > > https://arxiv.org/abs/1704.05770 > > > > Dan > > > > -- > > 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. > > -- > 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. --00000000000045adf60573c40482 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Ah, indeed, I misread the proposed definition.

<= div class=3D"gmail_quote">
Den l=C3=B6r 18 aug. 2018 21:35D= an Christensen <jdc@uwo.ca> skrev:<= br>
The extra identifications are one o= f the problems, but a more
fundamental problem is that while the north pole has been identified
with the south pole, no other pairs of antipodal points have been
identified.

Dan

On Aug 18, 2018, Guillaume Brunerie <guillaume.brunerie@gmail.= com> wrote:

> As Dan said, this is not a correct definition of RP^n.
>
> More specifically, the issue is that you identified the points "m= ap south" and "map north" in two different ways: "glue = south north" and
> "inv (glue north south)".
> You could try to add another constructor
> glue=C2=B2 : (x y : S^n) -> glue x y =3D inv (glue y x)
> but of course you're now again identifying them in two different w= ays, so you've just shifted the problem one dimension up.
>
> Den l=C3=B6r 18 aug. 2018 16:46Dan Christensen <jdc@uwo.ca> skrev: >
>=C2=A0 On Aug 18, 2018, Ali Caglayan <alizter@gmail.com> wrote= :
>
>=C2=A0 > This screams to me an alternative definition for =E2=84=9D= =E2=84=99=E2=81=BF (and maybe =E2=84=82=E2=84=99=E2=81=BF,...)
>=C2=A0 >
>=C2=A0 > Inductive RP (n:=E2=84=95) :=3D
>=C2=A0 > | map : S=E2=81=BF -> RP n
>=C2=A0 > | glue : (x y:S=E2=81=B0) -> map(in x) =3D map(in y)
>=C2=A0 >
>=C2=A0 > Where in : S=E2=81=B0=E2=86=92S=E2=81=BF is the obvious inc= lusion map.
>
>=C2=A0 That HIT would be S^n with four edges attached: two edges connec= ting
>=C2=A0 the north pole to the south pole, and a self-loop at each pole. = So
>=C2=A0 homotopically it would be S^n wedged with a wedge of four circle= s.
>
>=C2=A0 To get the right space with the right bundle over it, see:
>
>=C2=A0 The real projective spaces in homotopy type theory
>=C2=A0 Ulrik Buchholtz, Egbert Rijke
>=C2=A0 https://arxiv.org/abs/1704.05770
>
>=C2=A0 Dan
>
>=C2=A0 --
>=C2=A0 You received this message because you are subscribed to the Goog= le Groups "Homotopy Type Theory" group.
>=C2=A0 To unsubscribe from this group and stop receiving emails from it= , send an email to
>=C2=A0 HomotopyTypeTheory+unsubscribe@go= oglegroups.com.
>=C2=A0 For more options, visit https://groups.googl= e.com/d/optout.

--
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@googl= egroups.com.
For more options, visit https://groups.google.com/d/op= tout.

--
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.
--00000000000045adf60573c40482--