From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCAPPKFHBUIL5DPB3MCRUBHSVGURS@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-x53e.google.com (mail-ed1-x53e.google.com [IPv6:2a00:1450:4864:20::53e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 42467ee0 for ; Sat, 18 Aug 2018 16:18:06 +0000 (UTC) Received: by mail-ed1-x53e.google.com with SMTP id r25-v6sf752751edc.7 for ; Sat, 18 Aug 2018 09:18:06 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1534609086; cv=pass; d=google.com; s=arc-20160816; b=qU/okwnfj5k+/1neWKvjNvmJNZx6hKr33DeG+si/1Ndf0bTUJvZocv+gFgD/41An4D sJ3JKsYNBq41ZCnfU83798sdnLOXXK/U5tuMxBXDVCVYitenAdHS2wdhyAKAgf1EH1BI poZocKQPg6Y0SsSV5oD8T2wHpcBbXsdsvN7LeOrRbLeJt9E0+YqWNUKOjUHbKjRkEhKp 9NJRTM24r32BOQcWLWO/lxOTMLTmCEsbJeFhMHX8d49ct/oxYfvR4+5is6HbWqveyq8x laZuiCt3l9lvDQ+WBRGKgfP6tfRPXRHbXddOBJPAEnydxhc+JoAeFta+GEb2bEgP+6YP Pcqw== 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=pQekGE2wbPF51l7DDG5u/0ktls1Cqu7d3DntzAsTGjE=; b=rOhr4o+ZmlVhybbsSBj4Lnwdp0R9s7t3G0RD5xyu8DC0894oBDjoxjxi9pFrqlg7Nt 25+cFNIQb88ZNCeXERgil3do5RxywQvRW1I+zFQ4M+hkC1j7Tl6U+b5k8trv2tdWaZOU G+XAtVCMY5ivjPZ/vwuGSMXzxbs3S4ghQQ/VSj2Eq2YglD4nVAsUfB6LvLYpjJdrzxnz s8h/wNCQ8sMwkeQxl/WriNJai9NToMcoZ/Zr3rH0+i+H9lNth2IYB2ZnF3afq+IECHRy F4VzB/ALAwaGqgfLoTFL87ZhovRCRlItoZBn0caonmYv1UKgJAFGAr45C5RFAVzGIKIJ Eoyw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=MYPRcuAn; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::230 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=pQekGE2wbPF51l7DDG5u/0ktls1Cqu7d3DntzAsTGjE=; b=cOcavHecYvMV+8KlKkSPtLbRul5el1L6dmGYJ2nijQK4foybEvb10GeXCflIGnhFLr ohm+4A44lDwhxqAMtDRLuz922etJ9HA0szuyO6ggnx8LAb41RfMBoBCgZmYKBcsN3Cm1 Xog4/T2L1P2RrVdoXnnPGK+94VRAib2c5gm0mYadYh30UMTy5FFY1CW+mijIR0esZbYS Pp3I5jb+YkcXxVfnLrPekMYpY8ydux46L6jF7+oSGidN8FplT1k5JAJsWxcYVEmMgBi1 vpi0mzOGpVi/Y4Gg5z1rc3i6Y1ArRkrPsxHXL2dG6EF1KqWQtFCSGrhDhtY9z/ZVWRJ8 ocRQ== 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=pQekGE2wbPF51l7DDG5u/0ktls1Cqu7d3DntzAsTGjE=; b=LiwDdmj7Rezkx1S1mf5joa0ugvMe1TONaAN3uN4ZQF69cRYHKYnE46s9ZqePGJ9Xhl fCaSs1BI377X5zjXsY60zyZOLFF8+wzJ0yu9iCAHos8WuveHlTosjcqdN2wrL0Hk8gv6 C2nAVKmYtzylfPesvC0O5kaPXfb+eM20Cg2SegX4QYgFsIsrRfg9pt+jyw3F7ekSvhJc PfiJoyQo3aDMgNowQxqKjQm6Gn8vN0SzfazAm9H2doNXjhtopypyo7pBQXu/ngyRJveH ii5kMWIXZ4+o7ofZqpsLVQUczHmD5U9nQkFHQ0oJ9BZKVA+ZlhdcU0+zkC0xy35O3s6H MuNQ== 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=pQekGE2wbPF51l7DDG5u/0ktls1Cqu7d3DntzAsTGjE=; b=s2xR12Ap08TxNcdG4QN+xK515xSqCN3ElPQQ6hpCCHyrJLbA1nan/Z0f9r9trRL5AW 0lyPpJOOVoyPUsBQwoXwgyO+s9Z/r8ycKLbEnh7mDMfFixGm+FseXkj32bhCesIiCf0g Rbr/TaTiC026YZ8AscjE4bANC3X/p76xjpkeVYDILdR0CUq8Jq392SrkbW2yND4sTk43 +uM8JjVW3Bma3NVBrzm9n9DsEvj13cJkNCxf/REN8C2cuVPHXlZkuVV9LtZttVDBIkof TTN8MBHuhbGsBuc64hUvuyWl9kpsVTN5vC2KmgjLKDj5RimhJTeVq6xnWzNZhRoDcGjZ wdRw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFLqPMdU5ywyIg+gsT9BFb87MhvCspD8TxvghlBnijMr9tYk8iP RK+bQv6Mi/oJckjV/guvqPw= X-Google-Smtp-Source: AA+uWPy1UjKYvWMG3yEXcTp7PfgQ7bsa6TMHAb41SCMjQfuS0xpAQ5ZDY0GCRT0+tPf6g+Nso22Wxw== X-Received: by 2002:aa7:c24d:: with SMTP id y13-v6mr224270edo.2.1534609086194; Sat, 18 Aug 2018 09:18:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:d382:: with SMTP id x2-v6ls5037177edq.2.gmail; Sat, 18 Aug 2018 09:18:05 -0700 (PDT) X-Received: by 2002:aa7:c0c2:: with SMTP id j2-v6mr10426045edp.0.1534609085651; Sat, 18 Aug 2018 09:18:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1534609085; cv=none; d=google.com; s=arc-20160816; b=FK/XXGvhARu/yCoVU+2iwXdwOztfy1zcXbNKnSbbssrIgWV5ym0jcjb4a0RO8o7QJ3 TNayftYxS0ij8rDpfsePOwgCVs4qOWxs6vkHJapkAYS+PbFqXdGKonAoC2wgJ67t7khW u6t0O9YaDSXmjplLkT5MJMWDuZnW2HHO7RPvNXhpRR/vBjOfEnTaehGb4ZyatoMFBHJa 2nURtlrWA3DrvMKxEE6E5ghLX2Rqk+JwMkQcBcTg/K+xjqksHdEXoh9KRoP4PBBF3bXc P/Ze21LVEKAcET6hXLn34IRtfJ+fLA+lt3/rQPwP8W0mtTcJJrEXIyEBS/ncW3mY19cj +0MQ== 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=nRCW3XJ1ugqTTmYXjCCFmrsc/2VRSoD70hPEi25Utpk=; b=mT/5AYF3XePKSKozmb0mbVCIrSxHZ5WPYOSkPK6DhwLqLc5wHGQJVo8D6oANkK5yXg N1OHA2+FZtO1Z8GpGtIF0YgK4lGTnV/ZdtmQ4nJ980Ag0K31sMIpC8x1yykn+SB1LWo0 ItcwxNfVQpHg+pWJd1BL/LCvWhBm3hnXnh0xAm/O3ShJDMlaImuFE2gAmdgY9v9N7iy4 7zaO9veiC5eZhUgg+5SjwBNk+At3kRSwrJ3e/oXdoOCaKp8bx/kPXU2obPaYj5qUJHF8 VCiKmVfCeOAG7v4c5XbuXm02GPKwdDPEOngS8ckOdZ/7NsrG4T77t/L0t1F57Kv347YC AnVg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=MYPRcuAn; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::230 as permitted sender) smtp.mailfrom=guillaume.brunerie@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lj1-x230.google.com (mail-lj1-x230.google.com. [2a00:1450:4864:20::230]) by gmr-mx.google.com with ESMTPS id o55-v6si117404edo.3.2018.08.18.09.18.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 18 Aug 2018 09:18:05 -0700 (PDT) Received-SPF: pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::230 as permitted sender) client-ip=2a00:1450:4864:20::230; Received: by mail-lj1-x230.google.com with SMTP id p10-v6so8611707ljg.2 for ; Sat, 18 Aug 2018 09:18:05 -0700 (PDT) X-Received: by 2002:a2e:9941:: with SMTP id r1-v6mr26034318ljj.53.1534609084989; Sat, 18 Aug 2018 09:18:04 -0700 (PDT) MIME-Version: 1.0 References: <874lfrhgwo.fsf@uwo.ca> In-Reply-To: <874lfrhgwo.fsf@uwo.ca> From: Guillaume Brunerie Date: Sat, 18 Aug 2018 18:17:52 +0200 Message-ID: Subject: Re: [HoTT] Real Projective space (and other projective spaces too) To: alizter@gmail.com Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000061469e0573b805ff" 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=MYPRcuAn; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::230 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: , --00000000000061469e0573b805ff Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 map. > > 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. > --=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. --00000000000061469e0573b805ff Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
As Dan said, this is not a correct definition of RP^= n.

More specifically, th= e issue is that you identified the points "map south" and "m= ap north" in two different ways: "glue south north" and &quo= t;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 shift= ed the problem one dimension up.=C2=A0

Den l=C3=B6r 18 aug. 2018 16:46Dan Christensen = <jdc@uwo.ca> skrev:
On= Aug 18, 2018, Ali Caglayan <alizter@gmail.com&= gt; 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 map.=

That HIT would be S^n with four edges attached:=C2=A0 two edges connecting<= br> the north pole to the south pole, and a self-loop at each pole.=C2=A0 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:

=C2=A0 The real projective spaces in homotopy type theory
=C2=A0 Ulrik Buchholtz, Egbert Rijke
=C2=A0 https://arxiv.org/abs/1704.0= 5770

Dan

--
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 HomotopyTypeTh= eory+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 &= 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.
--00000000000061469e0573b805ff--